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