let z be Quaternion; :: thesis: |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)
((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) >= 0 by QUATERNI:74;
then |.z.| ^2 = sqrt ((((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) ^2) by SQUARE_1:29
.= ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by QUATERNI:74, SQUARE_1:22 ;
hence |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) ; :: thesis: verum