set C = Cayley-Dickson N;
let a be Element of (Cayley-Dickson N); :: according to ALGSTR_1:def 2 :: thesis: (0. (Cayley-Dickson N)) + a = a
consider a1, b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
A2: 0. (Cayley-Dickson N) = <%(0. N),(0. N)%> by Def9;
( (0. N) + a1 = a1 & (0. N) + b1 = b1 ) by ALGSTR_1:def 2;
hence (0. (Cayley-Dickson N)) + a = a by A1, A2, Def9; :: thesis: verum