set C = Cayley-Dickson N;
set f = the addF of (Cayley-Dickson N);
let a, b, c be Element of (Cayley-Dickson N); RLVECT_1:def 3 (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
;
verum