let z be quaternion number ; :: thesis: ( |.z.| = 0 implies z = 0 )
assume A1: |.z.| = 0 ; :: thesis: z = 0
A2: ( 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 A2;
then 0 = ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) by A1, SQUARE_1:93;
then ( Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by Lm8;
hence z = 0 by Lm5, Th24; :: thesis: verum