let z be Quaternion; :: thesis: ( z *' = 0 implies z = 0 )
assume A1: z *' = 0 ; :: thesis: z = 0
A2: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th36;
A3: Rea (z *') = 0 by A1, Lm6, Th16;
A4: Im1 (z *') = 0 by A1, Lm6, Th16;
A5: Im2 (z *') = 0 by A1, Lm6, Th16;
A6: Im3 (z *') = 0 by A1, Lm6, Th16;
A7: Rea (z *') = Rea z by A2, Th16;
A8: Im1 (z *') = - (Im1 z) by A2, Th16;
A9: Im2 (z *') = - (Im2 z) by A2, Th16;
Im3 (z *') = - (Im3 z) by A2, Th16;
hence z = 0 by A3, A4, A5, A6, A7, A8, A9, Th19; :: thesis: verum