let z be Quaternion; :: thesis: for x being Real st z = x holds
( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
let x be Real; :: thesis: ( z = x implies ( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) )
assume A1: z = x ; :: thesis: ( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
reconsider xx = x, zz = 0 as Element of REAL by XREAL_0:def 1;
A2: x = [*xx,zz*] by ARYTM_0:def 5;
[*xx,zz*] = [*x,0,0,0*] by Lm3;
hence ( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by A1, A2, Th16; :: thesis: verum