set C = Cayley-Dickson N;
let a be Element of (Cayley-Dickson N); :: according to RLVECT_1:def 4 :: thesis: a + (0. (Cayley-Dickson N)) = 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;
( a1 + (0. N) = a1 & b1 + (0. N) = b1 ) by RLVECT_1:def 4;
hence a + (0. (Cayley-Dickson N)) = a by A1, A2, Def9; :: thesis: verum