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

proof

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

end;

assume A4: not z in COMPLEX ; :: thesis: ex b₁ being Number ex f being Function of 4,REAL st
( z = f & b₁ = f . 1 )
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 A4, XBOOLE_0:def 3;
then reconsider f = z as Function of 4,REAL by FUNCT_2:66;
take f . 1 ; :: thesis: ex f being Function of 4,REAL st
( z = f & f . 1 = f . 1 )
take f ; :: thesis: ( z = f & f . 1 = f . 1 )
thus ( z = f & f . 1 = f . 1 ) ; :: thesis: verum