let a, b, c be Element of (Cayley-Dickson N); :: according to VECTSP_1:def 2 :: thesis: a * (b + c) = (a * b) + (a * c)
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: a1 * (b1 + c1) = (a1 * b1) + (a1 * c1) by VECTSP_1:def 2;
A5: (b2 + c2) * a1 = (b2 * a1) + (c2 * a1) by VECTSP_1:def 3;
(b2 + c2) *' = (b2 *') + (c2 *') by Def5;
then ((b2 + c2) *') * a2 = ((b2 *') * a2) + ((c2 *') * a2) by VECTSP_1:def 3;
then A6: (a1 * (b1 + c1)) - (((b2 + c2) *') * a2) = (((a1 * b1) + (a1 * c1)) - ((b2 *') * a2)) - ((c2 *') * a2) by A4, RLVECT_1:27
.= (((a1 * b1) - ((b2 *') * a2)) + (a1 * c1)) - ((c2 *') * a2) by RLVECT_1:def 3
.= ((a1 * b1) - ((b2 *') * a2)) + ((a1 * c1) - ((c2 *') * a2)) by RLVECT_1:def 3 ;
(b1 + c1) *' = (b1 *') + (c1 *') by Def5;
then a2 * ((b1 + c1) *') = (a2 * (b1 *')) + (a2 * (c1 *')) by VECTSP_1:def 2;
then A7: ((b2 + c2) * a1) + (a2 * ((b1 + c1) *')) = (((b2 * a1) + (c2 * a1)) + (a2 * (b1 *'))) + (a2 * (c1 *')) by A5, RLVECT_1:def 3
.= (((b2 * a1) + (a2 * (b1 *'))) + (c2 * a1)) + (a2 * (c1 *')) by RLVECT_1:def 3
.= ((b2 * a1) + (a2 * (b1 *'))) + ((c2 * a1) + (a2 * (c1 *'))) by RLVECT_1:def 3 ;
A8: a * b = <%((a1 * b1) - ((b2 *') * a2)),((b2 * a1) + (a2 * (b1 *')))%> by A1, A2, Def9;
A9: a * c = <%((a1 * c1) - ((c2 *') * a2)),((c2 * a1) + (a2 * (c1 *')))%> by A1, A3, Def9;
b + c = <%(b1 + c1),(b2 + c2)%> by A2, A3, Def9;
hence a * (b + c) = <%((a1 * (b1 + c1)) - (((b2 + c2) *') * a2)),(((b2 + c2) * a1) + (a2 * ((b1 + c1) *')))%> by A1, Def9
.= (a * b) + (a * c) by A6, A7, A8, A9, Def9 ;
:: thesis: verum