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