set C = Cayley-Dickson N;
let a be Element of (Cayley-Dickson N); :: according to ALGSTR_0:def 15 :: thesis: a is left_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: a2 + a1 = 0. N by ALGSTR_0:def 10;
consider b2 being Element of N such that
A3: b2 + b1 = 0. N by ALGSTR_0:def 10;
take <%a2,b2%> ; :: according to ALGSTR_0:def 10 :: thesis: <%a2,b2%> + a = 0. (Cayley-Dickson N)
0. (Cayley-Dickson N) = <%(0. N),(0. N)%> by Def9;
hence <%a2,b2%> + a = 0. (Cayley-Dickson N) by A1, A2, A3, Def9; :: thesis: verum