let a, b, c, d be 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 Lm5;
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:92;
then {0,1,2,3} c= {0,1} by FUNCT_4:137;
then {0,1} \/ {2,3} c= {0,1} by ENUMSET1:5;
hence contradiction by XBOOLE_1:11, ZFMISC_1:22; :: 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