let c be Quaternion; :: thesis: ( Rea (c .|. c) = |.c.| ^2 & Im1 (c .|. c) = 0 & Im2 (c .|. c) = 0 & Im2 (c .|. c) = 0 )
A1: ((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2) >= 0 by Lm2;
c .|. c = [*(((((Rea c) * (Rea c)) + ((Im1 c) * (Im1 c))) + ((Im2 c) * (Im2 c))) + ((Im3 c) * (Im3 c))),(((((Rea c) * (- (Im1 c))) + ((Im1 c) * (Rea c))) - ((Im2 c) * (Im3 c))) + ((Im3 c) * (Im2 c))),(((((Rea c) * (- (Im2 c))) + ((Rea c) * (Im2 c))) - ((Im1 c) * (Im3 c))) + ((Im3 c) * (Im1 c))),(((((Rea c) * (- (Im3 c))) + ((Im3 c) * (Rea c))) - ((Im1 c) * (Im2 c))) + ((Im2 c) * (Im1 c)))*] by Th48
.= [*(|.c.| ^2),0,0,0*] by A1, SQUARE_1:def 2 ;
hence ( Rea (c .|. c) = |.c.| ^2 & Im1 (c .|. c) = 0 & Im2 (c .|. c) = 0 & Im2 (c .|. c) = 0 ) by QUATERNI:23; :: thesis: verum