set C = Cayley-Dickson N;
0. (Cayley-Dickson N) = <%(0. N),(0. N)%> by Def9;
hence ||.(0. (Cayley-Dickson N)).|| = sqrt ((||.(0. N).|| ^2) + (||.(0. N).|| ^2)) by Def9
.= 0 ;
:: according to NORMSP_0:def 6 :: thesis: verum