set C = Cayley-Dickson N;
set f = the addF of (Cayley-Dickson N);
let a, b, c be Element of (Cayley-Dickson N); :: according to RLVECT_1:def 3 :: thesis: (a + b) + c = a + (b + c)
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;
consider a3, b3 being Element of N such that
A3: c = <%a3,b3%> by Th12;
A4: ( (a1 + a2) + a3 = a1 + (a2 + a3) & (b1 + b2) + b3 = b1 + (b2 + b3) ) by RLVECT_1:def 3;
A5: the addF of (Cayley-Dickson N) . (b,c) = <%(a2 + a3),(b2 + b3)%> by A2, A3, Def9;
the addF of (Cayley-Dickson N) . (a,b) = <%(a1 + a2),(b1 + b2)%> by A1, A2, Def9;
hence (a + b) + c = <%((a1 + a2) + a3),((b1 + b2) + b3)%> by A3, Def9
.= a + (b + c) by A1, A4, A5, Def9 ;
:: thesis: verum