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 & Im1 (z *' ) = 0 & Im2 (z *' ) = 0 & Im3 (z *' ) = 0 ) by A1, Lm5, Th23;
( Rea (z *' ) = Rea z & Im1 (z *' ) = - (Im1 z) & Im2 (z *' ) = - (Im2 z) & Im3 (z *' ) = - (Im3 z) ) by A2, Th23;
hence z = 0 by A3, Th26; :: thesis: verum