set C = Cayley-Dickson N;
let a, b be Element of (Cayley-Dickson N); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
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;
the addF of (Cayley-Dickson N) . (a,b) = <%(a1 + a2),(b1 + b2)%> by A1, A2, Def9;
hence a + b = b + a by A1, A2, Def9; :: thesis: verum