thus ( z is real implies ex IT being set st IT = 0 ) ; :: thesis: ( not z is real implies ex b₁ being number ex f being Function of 2,REAL st
( z = f & b₁ = f . 1 ) )
A2: 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 . 1 )
then not z in REAL ;
then z in (Funcs (2,REAL)) \ { x where x is Element of Funcs (2,REAL) : x . 1 = 0 } by A2, 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 . 1 ; :: thesis: ex f being Function of 2,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