let z be Quaternion; ( Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = 0q )
assume that
A1:
Rea z = 0
and
A2:
Im1 z = 0
and
A3:
Im2 z = 0
and
A4:
Im3 z = 0
; z = 0q
A5:
Rea z = Rea [*0,0,0,0*]
by A1, Th16;
A6:
Im1 z = Im1 [*0,0,0,0*]
by A2, Th16;
A7:
Im2 z = Im2 [*0,0,0,0*]
by A3, Th16;
Im3 z = Im3 [*0,0,0,0*]
by A4, Th16;
hence
z = 0q
by A5, A6, A7, Lm6, Th18; verum