set C = Cayley-Dickson N;
let c be Element of (Cayley-Dickson N); :: according to CAYLDICK:def 4 :: thesis: c is well-conjugated
consider a, b being Element of N such that
A1: c = <%a,b%> by Th12;
A2: 0. (Cayley-Dickson N) = <%(0. N),(0. N)%> by Def9;
A3: c *' = <%(a *'),(- b)%> by A1, Def9;
A4: ||.c.|| = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) by A1, Def9;
per cases ( not c is zero or c is zero ) ;
:: according to CAYLDICK:def 3
case not c is zero ; :: thesis: (c *') * c = (||.c.|| ^2) * (1. (Cayley-Dickson N))
A5: 1. (Cayley-Dickson N) = <%(1. N),(0. N)%> by Def9;
A6: ( (a *') * a = (||.a.|| ^2) * (1. N) & (b *') * b = (||.b.|| ^2) * (1. N) ) by Th9;
A7: ((a *') * a) - ((b *') * (- b)) = ((a *') * a) - (- ((b *') * b)) by VECTSP_1:8
.= ((a *') * a) + ((b *') * b)
.= ((||.a.|| ^2) + (||.b.|| ^2)) * (1. N) by A6, RLVECT_1:def 6
.= (||.c.|| ^2) * (1. N) by A4, SQUARE_1:def 2 ;
b + (- b) = 0. N by RLVECT_1:def 10;
then (b * (a *')) + ((- b) * (a *')) = (0. N) * (a *') by VECTSP_1:def 3
.= (||.c.|| ^2) * (0. N) ;
then (c *') * c = <%((||.c.|| ^2) * (1. N)),((||.c.|| ^2) * (0. N))%> by A1, A3, A7, Def9
.= (||.c.|| ^2) * (1. (Cayley-Dickson N)) by A5, Def9 ;
hence (c *') * c = (||.c.|| ^2) * (1. (Cayley-Dickson N)) ; :: thesis: verum
end;
case c is zero ; :: thesis: c *' is zero
then c = 0. (Cayley-Dickson N) ;
then A8: ( a = 0. N & b = 0. N ) by A1, A2, Th3;
||.(c *').|| = 0 by A3, A8;
hence c *' = 0. (Cayley-Dickson N) by NORMSP_0:def 5; :: according to STRUCT_0:def 12 :: thesis: verum
end;
end;