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