let z be quaternion number ; :: thesis: ( z = 0 implies z *' = 0 )
assume z = 0 ; :: thesis: z *' = 0
then ( Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by Lm5, Th23;
hence z *' = 0 by Lm5, Th43; :: thesis: verum