let z be quaternion number ; :: thesis: 0 <= |.z.|
A1: ( 0 <= (Rea z) ^2 & 0 <= (Im1 z) ^2 & 0 <= (Im2 z) ^2 & 0 <= (Im3 z) ^2 ) by XREAL_1:65;
0 <= ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) by A1;
hence 0 <= |.z.| by SQUARE_1:def 4; :: thesis: verum