thus ( z is real implies ex IT being set st IT = z ) :: thesis: ( not z is real implies ex b₁ being number ex f being Function of 2,REAL st
( z = f & b₁ = f . 0 ) )

proof

assume z is real ; :: thesis: ex IT being set st IT = z
then z in REAL by XREAL_0:def 1;
hence ex IT being set st IT = z ; :: thesis: verum

end;

A1: z in COMPLEX by XCMPLX_0:def 2;
assume not z is real ; :: thesis: ex b₁ being number ex f being Function of 2,REAL st
( z = f & b₁ = f . 0 )
then not z in REAL ;
then z in (Funcs (2,REAL)) \ { x where x is Element of Funcs (2,REAL) : x . 1 = 0 } by A1, CARD_1:50, NUMBERS:def 2, XBOOLE_0:def 3;
then reconsider f = z as Function of 2,REAL by FUNCT_2:66;
take f . 0 ; :: thesis: ex f being Function of 2,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