let a, b, c, d be Real; 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)
;
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;
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; verum