let z be Quaternion; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum