set C = Cayley-Dickson N;
A1: ||.(1. N).|| = 1 by LOPBAN_2:def 10;
1. (Cayley-Dickson N) = <%(1. N),(0. N)%> by Def9;
hence ||.(1. (Cayley-Dickson N)).|| = sqrt ((||.(1. N).|| ^2) + (||.(0. N).|| ^2)) by Def9
.= 1 by A1, SQUARE_1:18 ;
:: according to LOPBAN_2:def 10 :: thesis: verum