let z be quaternion number ; :: thesis: ( z is Real implies ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) )
assume A1: z is Real ; :: thesis: ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
reconsider x = z as Real by A1;
A2: ( x = [*x,0 *] & [*x,0 *] = [*x,0 ,0 ,0 *] ) by ARYTM_0:def 7, QUATERNI:91;
thus ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by A2, QUATERNI:23; :: thesis: verum