defpred S1[ set , set ] means for phi being Element of Funcs (F1(),F2()) st phi | F3() = \$1 holds
\$2 = F5(phi);
set Z = { F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4() } ;
set x = the Element of { F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4() } ;
A4: F2() /\ F4() c= F2() by XBOOLE_1:17;
assume A5: not { F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4() } is finite ; :: thesis: contradiction
then { F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4() } <> {} ;
then the Element of { F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4() } in { F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4() } ;
then consider phi being Element of Funcs (F1(),F2()) such that
the Element of { F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4() } = F5(phi) and
A6: phi .: F3() c= F4() ;
now :: thesis: ( F2() /\ F4() = {} implies F1() /\ F3() = {} )
assume F2() /\ F4() = {} ; :: thesis: F1() /\ F3() = {}
then A7: phi .: F3() = {} by ;
F1() = dom phi by FUNCT_2:def 1;
then F1() misses F3() by ;
hence F1() /\ F3() = {} ; :: thesis: verum
end;
then reconsider FF = Funcs ((F1() /\ F3()),(F2() /\ F4())), Z = { F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4() } as non empty set by ;
A8: F2() /\ F4() c= F4() by XBOOLE_1:17;
A9: F1() /\ F3() c= F1() by XBOOLE_1:17;
A10: now :: thesis: for f being Element of FF ex g being Element of Z st S1[f,g]
let f be Element of FF; :: thesis: ex g being Element of Z st S1[f,g]
consider phi being Element of Funcs (F1(),F2()) such that
A11: phi | (F1() /\ F3()) = f by A9, A4, Th4;
A12: phi | F3() = f by ;
ex g being Function st
( f = g & dom g = F1() /\ F3() & rng g c= F2() /\ F4() ) by FUNCT_2:def 2;
then rng (phi | F3()) c= F4() by ;
then phi .: F3() c= F4() by RELAT_1:115;
then F5(phi) in Z ;
then reconsider g9 = F5(phi) as Element of Z ;
take g = g9; :: thesis: S1[f,g]
thus S1[f,g] by A3, A12; :: thesis: verum
end;
consider F being Function of FF,Z such that
A13: for f being Element of FF holds S1[f,F . f] from Z c= F .: (Funcs ((F1() /\ F3()),(F2() /\ F4())))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Z or y in F .: (Funcs ((F1() /\ F3()),(F2() /\ F4()))) )
assume y in Z ; :: thesis: y in F .: (Funcs ((F1() /\ F3()),(F2() /\ F4())))
then consider phi being Element of Funcs (F1(),F2()) such that
A14: y = F5(phi) and
A15: phi .: F3() c= F4() ;
rng (phi | F3()) c= F4() by ;
then A16: rng (phi | F3()) c= F2() /\ F4() by XBOOLE_1:19;
A17: dom (phi | F3()) = (dom phi) /\ F3() by RELAT_1:61
.= F1() /\ F3() by FUNCT_2:def 1 ;
then reconsider x = phi | F3() as Element of Funcs ((F1() /\ F3()),(F2() /\ F4())) by ;
phi | F3() in Funcs ((F1() /\ F3()),(F2() /\ F4())) by ;
then A18: x in dom F by FUNCT_2:def 1;
y = F . x by ;
hence y in F .: (Funcs ((F1() /\ F3()),(F2() /\ F4()))) by ; :: thesis: verum
end;
hence contradiction by A1, A2, A5; :: thesis: verum