Solution (source code)

= Solution

\b[True.] This is left distributivity of <ordinal multiplication>. Fix $\alpha,\beta$ and induct on $\gamma$. The zero case is immediate. The successor step uses $\alpha(\eta+1)=\alpha\eta+\alpha$ and <associativity of ordinal addition>. At a limit, multiplication and addition are <continuous> in their right argument, so taking suprema of the earlier equalities gives $\alpha(\beta+\gamma)=\alpha\beta+\alpha\gamma$.