let c be quaternion number ; :: thesis: c .|. c = |.c.| ^2
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
.= [*(((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2)),0*] by QUATERNI:91
.= ((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2) by ARYTM_0:def 7
.= |.c.| ^2 by A1, SQUARE_1:def 4 ;
hence c .|. c = |.c.| ^2 ; :: thesis: verum