let z be Quaternion; :: thesis: ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = Rea z )
set x = Rea z;
assume ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) ; :: thesis: z = Rea z
then A1: z = [*(Rea z),0,0,0*] by QUATERNI:24;
reconsider xx = Rea z, zz = 0 as Element of REAL by XREAL_0:def 1;
[*(Rea z),0,0,0*] = [*xx,zz*] by QUATERNI:91;
hence z = Rea z by A1, ARYTM_0:def 5; :: thesis: verum