let a, b, c, d be Element of REAL ; :: thesis: not 0 ,1,2,3 --> a,b,c,d in COMPLEX
set f = 0 ,1,2,3 --> a,b,c,d;
A1: not 0 ,1,2,3 --> a,b,c,d in REAL by Lm6;
not 0 ,1,2,3 --> a,b,c,d in Funcs {0 ,1},REAL

proof

assume 0 ,1,2,3 --> a,b,c,d in Funcs {0 ,1},REAL ; :: thesis: contradiction
then dom (0 ,1,2,3 --> a,b,c,d) = {0 ,1} by FUNCT_2:169;
then {0 ,1,2,3} c= {0 ,1} by Th1;
then {0 ,1} \/ {2,3} c= {0 ,1} by ENUMSET1:45;
hence contradiction by XBOOLE_1:11, ZFMISC_1:28; :: thesis: verum

end;

then not 0 ,1,2,3 --> a,b,c,d in (Funcs {0 ,1},REAL ) \ { x where x is Element of Funcs {0 ,1},REAL : x . 1 = 0 } ;
hence not 0 ,1,2,3 --> a,b,c,d in COMPLEX by A1, NUMBERS:def 2, XBOOLE_0:def 3; :: thesis: verum