let z be quaternion number ; :: thesis: ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z *' = z )
assume A1: ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) ; :: thesis: z *' = z
then A2: z = [*(Rea z),0 ,0 ,0 *] by Th24
.= [*(Rea z),0 *] by Def6'
.= Rea z by ARYTM_0:def 7 ;
z *' = [*(Rea z),0 ,0 ,0 *] by A1, Th43
.= [*(Rea z),0 *] by Def6'
.= Rea z by ARYTM_0:def 7 ;
hence z *' = z by A2; :: thesis: verum