let z be quaternion number ; :: 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 Real ;
( x = [*x,0*] & [*x,0*] = [*x,0,0,0*] ) by ARYTM_0:def 7, QUATERNI:91;
hence ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by QUATERNI:23; :: thesis: verum