set X = { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ;

rng ((0,1) --> (0,1)) c= {(In (0,REAL)),1} by FUNCT_4:62, Lm1;

then rng ((0,1) --> (0,1)) c= REAL by A2, XBOOLE_1:1;

then <i> is Relation of {0,1},REAL by RELSET_1:6;

then <i> in Funcs ({0,1},REAL) by FUNCT_2:8;

then <i> in (Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } by A1, XBOOLE_0:def 5;

hence <i> in COMPLEX by NUMBERS:def 2, XBOOLE_0:def 3; :: according to XCMPLX_0:def 2 :: thesis: verum

A1: now :: thesis: not <i> in { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 }

A2:
{(In (0,REAL)),1} c= REAL
by ZFMISC_1:32, Lm2;assume
<i> in { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 }
; :: thesis: contradiction

then ex x being Element of Funcs ({0,1},REAL) st

( <i> = x & x . 1 = 0 ) ;

hence contradiction by FUNCT_4:63; :: thesis: verum

end;then ex x being Element of Funcs ({0,1},REAL) st

( <i> = x & x . 1 = 0 ) ;

hence contradiction by FUNCT_4:63; :: thesis: verum

rng ((0,1) --> (0,1)) c= {(In (0,REAL)),1} by FUNCT_4:62, Lm1;

then rng ((0,1) --> (0,1)) c= REAL by A2, XBOOLE_1:1;

then <i> is Relation of {0,1},REAL by RELSET_1:6;

then <i> in Funcs ({0,1},REAL) by FUNCT_2:8;

then <i> in (Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } by A1, XBOOLE_0:def 5;

hence <i> in COMPLEX by NUMBERS:def 2, XBOOLE_0:def 3; :: according to XCMPLX_0:def 2 :: thesis: verum