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

A1: now

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:66; :: thesis: verum

end;

<i> in Funcs ({0,1},REAL) by FUNCT_2:11;
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