let z be quaternion number ; :: thesis: ( z = 0 implies z *' = 0 )
assume A1: z = 0 ; :: thesis: z *' = 0
then A2: Rea z = 0 by Lm7, Th23;
A3: Im1 z = 0 by A1, Lm7, Th23;
A4: Im2 z = 0 by A1, Lm7, Th23;
Im3 z = 0 by A1, Lm7, Th23;
hence z *' = 0 by A2, A3, A4, Lm7, Th43; :: thesis: verum