let z be Quaternion; :: 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
reconsider Rz = Rea z, zz = 0 as Element of REAL by XREAL_0:def 1;
A4: z = [*(Rea z),0,0,0*] by A1, A2, A3, Th17
.= [*Rz,zz*] by Lm3
.= Rea z by ARYTM_0:def 5 ;
z *' = [*(Rea z),0,0,0*] by A1, A2, A3, Th36
.= [*Rz,zz*] by Lm3
.= Rea z by ARYTM_0:def 5 ;
hence z *' = z by A4; :: thesis: verum