let c1, c2 be Element of (Cayley-Dickson N); :: according to FUNCSDOM:def 9 :: thesis: for b₁ being object holds b₁ * (c1 * c2) = (b₁ * c1) * c2
let r be Real; :: thesis: r * (c1 * c2) = (r * c1) * c2
consider a1, b1 being Element of N such that
A1: c1 = <%a1,b1%> by Th12;
consider a2, b2 being Element of N such that
A2: c2 = <%a2,b2%> by Th12;
A3: c1 * c2 = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> by A1, A2, Def9;
A4: r * (a1 * a2) = (r * a1) * a2 by FUNCSDOM:def 9;
r * ((b2 *') * b1) = (b2 *') * (r * b1) by LOPBAN_2:def 11;
then A5: r * ((a1 * a2) - ((b2 *') * b1)) = ((r * a1) * a2) - ((b2 *') * (r * b1)) by A4, RLVECT_1:34;
A6: r * (b2 * a1) = b2 * (r * a1) by LOPBAN_2:def 11;
r * (b1 * (a2 *')) = (r * b1) * (a2 *') by FUNCSDOM:def 9;
then A7: r * ((b2 * a1) + (b1 * (a2 *'))) = (b2 * (r * a1)) + ((r * b1) * (a2 *')) by A6, RLVECT_1:def 5;
r * c1 = <%(r * a1),(r * b1)%> by A1, Def9;
hence (r * c1) * c2 = <%(((r * a1) * a2) - ((b2 *') * (r * b1))),((b2 * (r * a1)) + ((r * b1) * (a2 *')))%> by A2, Def9
.= r * (c1 * c2) by A3, A5, A7, Def9 ;
:: thesis: verum