let z be quaternion number ; :: thesis: ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z *' = z )
assume that
A1: Im1 z = 0 and
A2: Im2 z = 0 and
A3: Im3 z = 0 ; :: thesis: z *' = z
A4: z = [*(Rea z),0,0,0*] by A1, A2, A3, Th24
.= [*(Rea z),0*] by Lm4
.= Rea z by ARYTM_0:def 5 ;
z *' = [*(Rea z),0,0,0*] by A1, A2, A3, Th43
.= [*(Rea z),0*] by Lm4
.= Rea z by ARYTM_0:def 5 ;
hence z *' = z by A4; :: thesis: verum