let a be Element of (Cayley-Dickson N); :: according to CAYLDICK:def 6 :: thesis: ||.(a *').|| = ||.a.||
consider a1, a2 being Element of N such that
A1: a = <%a1,a2%> by Th12;
A2: ||.(a1 *').|| = ||.a1.|| by Def6;
A3: ||.(- a2).|| = ||.a2.|| by NORMSP_1:2;
a *' = <%(a1 *'),(- a2)%> by A1, Def9;
hence ||.(a *').|| = sqrt ((||.(a1 *').|| ^2) + (||.(- a2).|| ^2)) by Def9
.= ||.a.|| by A1, A2, A3, Def9 ;
:: thesis: verum