let z be Quaternion; ( |.z.| = 0 implies z = 0 )
assume A1:
|.z.| = 0
; 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; verum