let z be quaternion number ; :: thesis: ( z is real implies ( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) )
assume z is real ; :: thesis: ( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
then z in REAL by XREAL_0:def 1;
hence ( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by Lm19; :: thesis: verum