let z be Quaternion; :: thesis: ( |.z.| = 0 implies z = 0 )
assume A1: |.z.| = 0 ; :: thesis: z = 0
A2: 0 <= (Rea z) ^2 by XREAL_1:63;
A3: 0 <= (Im1 z) ^2 by XREAL_1:63;
A4: 0 <= (Im2 z) ^2 by XREAL_1:63;
0 <= (Im3 z) ^2 by XREAL_1:63;
then A5: 0 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by A1, A2, A3, A4, SQUARE_1:25;
then A6: Rea z = 0 by Lm9;
A7: Im1 z = 0 by A5, Lm9;
A8: Im2 z = 0 by A5, Lm9;
Im3 z = 0 by A5, Lm9;
hence z = 0 by A6, A7, A8, Lm6, Th17; :: thesis: verum