thus ( z in COMPLEX implies ex IT being Number ex z9 being Complex st
( z = z9 & IT = Re z9 ) ) :: thesis: ( not z in COMPLEX implies ex b₁ being Number ex f being Function of 4,REAL st
( z = f & b₁ = f . 0 ) )

proof

assume z in COMPLEX ; :: thesis: ex IT being Number ex z9 being Complex st
( z = z9 & IT = Re z9 )
then consider r, s being Element of REAL such that
A1: z = [*r,s*] by ARYTM_0:9;
set z9 = [*r,s*];
take Re [*r,s*] ; :: thesis: ex z9 being Complex st
( z = z9 & Re [*r,s*] = Re z9 )
take [*r,s*] ; :: thesis: ( z = [*r,s*] & Re [*r,s*] = Re [*r,s*] )
thus ( z = [*r,s*] & Re [*r,s*] = Re [*r,s*] ) by A1; :: thesis: verum

end;

assume A2: not z in COMPLEX ; :: thesis: ex b₁ being Number ex f being Function of 4,REAL st
( z = f & b₁ = f . 0 )
z in QUATERNION by Def2;
then z in (Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } by A2, XBOOLE_0:def 3;
then reconsider f = z as Function of 4,REAL by FUNCT_2:66;
take f . 0 ; :: thesis: ex f being Function of 4,REAL st
( z = f & f . 0 = f . 0 )
take f ; :: thesis: ( z = f & f . 0 = f . 0 )
thus ( z = f & f . 0 = f . 0 ) ; :: thesis: verum