thus ( y = 0 implies x is Element of COMPLEX ) by NUMBERS:def 2, XBOOLE_0:def 3; :: thesis: ( not y = 0 implies 0 ,1 --> x,y is Element of COMPLEX )
set z = 0 ,1 --> x,y;
assume A1: y <> 0 ; :: thesis: 0 ,1 --> x,y is Element of COMPLEX
A2: 0 ,1 --> x,y in Funcs {0 ,1},REAL by FUNCT_2:11;

now

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

end;

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 NUMBERS:def 2, XBOOLE_0:def 3; :: thesis: verum