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