let z be quaternion number ; :: thesis: |.(z * z).| = ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 )
A1: ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) >= 0 by Lm23;
|.z.| * |.z.| = (sqrt (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) ^2
.= ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) by A1, SQUARE_1:def 4 ;
hence |.(z * z).| = ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) by Th87; :: thesis: verum