let z be Quaternion; :: thesis: 0 <= |.z.|
A1: 0 <= (Rea z) ^2 by XREAL_1:63;
A2: 0 <= (Im1 z) ^2 by XREAL_1:63;
A3: 0 <= (Im2 z) ^2 by XREAL_1:63;
0 <= (Im3 z) ^2 by XREAL_1:63;
hence 0 <= |.z.| by A1, A2, A3, SQUARE_1:def 2; :: thesis: verum