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

A1: now

assume A2: <i> in { x where x is Element of Funcs {0 ,1},REAL : x . 1 = 0 } ; :: thesis: contradiction
A3: ex x being Element of Funcs {0 ,1},REAL st
( <i> = x & x . 1 = 0 ) by A2;
thus contradiction by A3, FUNCT_4:66; :: thesis: verum

end;

A4: <i> in Funcs {0 ,1},REAL by FUNCT_2:11;
A5: <i> in (Funcs {0 ,1},REAL ) \ { x where x is Element of Funcs {0 ,1},REAL : x . 1 = 0 } by A1, A4, XBOOLE_0:def 5;
thus <i> in COMPLEX by A5, NUMBERS:def 2, XBOOLE_0:def 3; :: according to XCMPLX_0:def 2 :: thesis: verum