set z = (0,1) --> (x,y);
thus
( y = 0 implies x is Element of COMPLEX )
by XBOOLE_0:def 3; ( not y = 0 implies (0,1) --> (x,y) is Element of COMPLEX )
assume A1:
y <> 0
; (0,1) --> (x,y) is Element of COMPLEX
(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; verum