set C = Cayley-Dickson N;
let a be Element of (Cayley-Dickson N); :: according to NORMSP_0:def 5 :: thesis: ( not ||.a.|| = 0 or a = 0. (Cayley-Dickson N) )
assume A1: ||.a.|| = 0 ; :: thesis: a = 0. (Cayley-Dickson N)
consider a1, b1 being Element of N such that
A2: a = <%a1,b1%> by Th12;
||.a.|| = sqrt ((||.a1.|| ^2) + (||.b1.|| ^2)) by A2, Def9;
then ( ||.a1.|| = 0 & ||.b1.|| = 0 ) by A1, SQUARE_1:24;
then ( a1 = 0. N & b1 = 0. N ) by NORMSP_0:def 5;
hence a = 0. (Cayley-Dickson N) by A2, Def9; :: thesis: verum