let a, b, c be Element of (Cayley-Dickson N); :: according to VECTSP_1:def 3 :: thesis: (b + c) * a = (b * a) + (c * a)
consider a1, a2 being Element of N such that
A1: a = <%a1,a2%> by Th12;
consider b1, b2 being Element of N such that
A2: b = <%b1,b2%> by Th12;
consider c1, c2 being Element of N such that
A3: c = <%c1,c2%> by Th12;
A4: b + c = <%(b1 + c1),(b2 + c2)%> by A2, A3, Def9;
A5: b * a = <%((b1 * a1) - ((a2 *') * b2)),((a2 * b1) + (b2 * (a1 *')))%> by A1, A2, Def9;
A6: c * a = <%((c1 * a1) - ((a2 *') * c2)),((a2 * c1) + (c2 * (a1 *')))%> by A1, A3, Def9;
A7: (b1 + c1) * a1 = (b1 * a1) + (c1 * a1) by VECTSP_1:def 3;
A8: a2 * (b1 + c1) = (a2 * b1) + (a2 * c1) by VECTSP_1:def 2;
(a2 *') * (b2 + c2) = ((a2 *') * b2) + ((a2 *') * c2) by VECTSP_1:def 2;
then A9: ((b1 + c1) * a1) - ((a2 *') * (b2 + c2)) = (((b1 * a1) + (c1 * a1)) - ((a2 *') * b2)) - ((a2 *') * c2) by A7, RLVECT_1:27
.= (((b1 * a1) - ((a2 *') * b2)) + (c1 * a1)) - ((a2 *') * c2) by RLVECT_1:28
.= ((b1 * a1) - ((a2 *') * b2)) + ((c1 * a1) - ((a2 *') * c2)) by RLVECT_1:28 ;
(b2 + c2) * (a1 *') = (b2 * (a1 *')) + (c2 * (a1 *')) by VECTSP_1:def 3;
then A10: (a2 * (b1 + c1)) + ((b2 + c2) * (a1 *')) = (((a2 * b1) + (a2 * c1)) + (b2 * (a1 *'))) + (c2 * (a1 *')) by A8, RLVECT_1:def 3
.= (((a2 * b1) + (b2 * (a1 *'))) + (a2 * c1)) + (c2 * (a1 *')) by RLVECT_1:def 3
.= ((a2 * b1) + (b2 * (a1 *'))) + ((a2 * c1) + (c2 * (a1 *'))) by RLVECT_1:def 3 ;
thus (b + c) * a = <%(((b1 + c1) * a1) - ((a2 *') * (b2 + c2))),((a2 * (b1 + c1)) + ((b2 + c2) * (a1 *')))%> by A1, A4, Def9
.= (b * a) + (c * a) by A5, A6, A9, A10, Def9 ; :: thesis: verum