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