set z = (0,1) --> (x,y);
thus ( y = 0 implies x is Element of COMPLEX ) by XBOOLE_0:def 3; :: thesis: ( not y = 0 implies (0,1) --> (x,y) is Element of COMPLEX )
assume A1: y <> 0 ; :: thesis: (0,1) --> (x,y) is Element of COMPLEX
A2: now :: thesis: not (0,1) --> (x,y) in { r where r is Element of Funcs ({0,1},REAL) : r . 1 = 0 }
assume (0,1) --> (x,y) in { r where r is Element of Funcs ({0,1},REAL) : r . 1 = 0 } ; :: thesis: contradiction
then ex r being Element of Funcs ({0,1},REAL) st
( (0,1) --> (x,y) = r & r . 1 = 0 ) ;
hence contradiction by A1, FUNCT_4:63; :: thesis: verum
end;
(0,1) --> (x,y) in Funcs ({0,1},REAL) by FUNCT_2:8;
then (0,1) --> (x,y) in (Funcs ({0,1},REAL)) \ { r where r is Element of Funcs ({0,1},REAL) : r . 1 = 0 } by A2, XBOOLE_0:def 5;
hence (0,1) --> (x,y) is Element of COMPLEX by XBOOLE_0:def 3; :: thesis: verum