set C = Cayley-Dickson N;
let a be Element of (Cayley-Dickson N); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
consider a1, b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
consider a2 being Element of N such that
A2: a1 + a2 = 0. N by ALGSTR_0:def 11;
consider b2 being Element of N such that
A3: b1 + b2 = 0. N by ALGSTR_0:def 11;
take <%a2,b2%> ; :: according to ALGSTR_0:def 11 :: thesis: a + <%a2,b2%> = 0. (Cayley-Dickson N)
0. (Cayley-Dickson N) = <%(0. N),(0. N)%> by Def9;
hence a + <%a2,b2%> = 0. (Cayley-Dickson N) by A1, A2, A3, Def9; :: thesis: verum