let z be quaternion number ; :: thesis: z ~ = |.z.| ^2
a: ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) >= 0 by QUATERNI:74;
|.z.| ^2 = sqrt ((((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 )) ^2 ) by a, SQUARE_1:97
.= ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) by QUATERNI:74, SQUARE_1:89 ;
hence z ~ = |.z.| ^2 ; :: thesis: verum