let z be quaternion number ; :: thesis: ( z *' = 0 implies z = 0 )
assume A1: z *' = 0 ; :: thesis: z = 0
A2: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th43;
A3: Rea (z *') = 0 by A1, Lm7, Th23;
A4: Im1 (z *') = 0 by A1, Lm7, Th23;
A5: Im2 (z *') = 0 by A1, Lm7, Th23;
A6: Im3 (z *') = 0 by A1, Lm7, Th23;
A7: Rea (z *') = Rea z by A2, Th23;
A8: Im1 (z *') = - (Im1 z) by A2, Th23;
A9: Im2 (z *') = - (Im2 z) by A2, Th23;
Im3 (z *') = - (Im3 z) by A2, Th23;
hence z = 0 by A3, A4, A5, A6, A7, A8, A9, Th26; :: thesis: verum