set C = Cayley-Dickson N;
( 0. (Cayley-Dickson N) = <%(0. N),(0. N)%> & 1. (Cayley-Dickson N) = <%(1. N),(0. N)%> ) by Def9;
hence 0. (Cayley-Dickson N) <> 1. (Cayley-Dickson N) ; :: according to STRUCT_0:def 8 :: thesis: verum