set X = { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ;
A1: now :: thesis: not <i> in { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 }
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;
A2: {(In (0,REAL)),1} c= REAL by ZFMISC_1:32, Lm2;
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