let c be Quaternion; :: thesis: c .|. c = |.c.| ^2
reconsider z = 0 , z1 = ((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2) as Element of REAL by XREAL_0:def 1;
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
.= [*z1,z*] by QUATERNI:91
.= ((((Rea c) ^2) + ((Im1 c) ^2)) + ((Im2 c) ^2)) + ((Im3 c) ^2) by ARYTM_0:def 5
.= |.c.| ^2 by A1, SQUARE_1:def 2 ;
hence c .|. c = |.c.| ^2 ; :: thesis: verum