defpred S₁[ set , set ] means for phi being Element of Funcs (F₁(),F₂()) st phi | F₃() = $1 holds
$2 = F₅(phi);
set Z = { F₅(phi9) where phi9 is Element of Funcs (F₁(),F₂()) : phi9 .: F₃() c= F₄() } ;
set x = the Element of { F₅(phi9) where phi9 is Element of Funcs (F₁(),F₂()) : phi9 .: F₃() c= F₄() } ;
A4: F₂() /\ F₄() c= F₂() by XBOOLE_1:17;
assume A5: not { F₅(phi9) where phi9 is Element of Funcs (F₁(),F₂()) : phi9 .: F₃() c= F₄() } is finite ; :: thesis: contradiction
then { F₅(phi9) where phi9 is Element of Funcs (F₁(),F₂()) : phi9 .: F₃() c= F₄() } <> {} ;
then the Element of { F₅(phi9) where phi9 is Element of Funcs (F₁(),F₂()) : phi9 .: F₃() c= F₄() } in { F₅(phi9) where phi9 is Element of Funcs (F₁(),F₂()) : phi9 .: F₃() c= F₄() } ;
then consider phi being Element of Funcs (F₁(),F₂()) such that
the Element of { F₅(phi9) where phi9 is Element of Funcs (F₁(),F₂()) : phi9 .: F₃() c= F₄() } = F₅(phi) and
A6: phi .: F₃() c= F₄() ;

now :: thesis: ( F₂() /\ F₄() = {} implies F₁() /\ F₃() = {} )

assume F₂() /\ F₄() = {} ; :: thesis: F₁() /\ F₃() = {}
then A7: phi .: F₃() = {} by A6, XBOOLE_1:3, XBOOLE_1:19;
F₁() = dom phi by FUNCT_2:def 1;
then F₁() misses F₃() by A7, RELAT_1:118;
hence F₁() /\ F₃() = {} ; :: thesis: verum

end;

then reconsider FF = Funcs ((F₁() /\ F₃()),(F₂() /\ F₄())), Z = { F₅(phi9) where phi9 is Element of Funcs (F₁(),F₂()) : phi9 .: F₃() c= F₄() } as non empty set by A5, FUNCT_2:8;
A8: F₂() /\ F₄() c= F₄() by XBOOLE_1:17;
A9: F₁() /\ F₃() c= F₁() by XBOOLE_1:17;

A10: now :: thesis: for f being Element of FF ex g being Element of Z st S₁[f,g]

let f be Element of FF; :: thesis: ex g being Element of Z st S₁[f,g]
consider phi being Element of Funcs (F₁(),F₂()) such that
A11: phi | (F₁() /\ F₃()) = f by A9, A4, Th4;
A12: phi | F₃() = f by A11, Th5;
ex g being Function st
( f = g & dom g = F₁() /\ F₃() & rng g c= F₂() /\ F₄() ) by FUNCT_2:def 2;
then rng (phi | F₃()) c= F₄() by A8, A12;
then phi .: F₃() c= F₄() by RELAT_1:115;
then F₅(phi) in Z ;
then reconsider g9 = F₅(phi) as Element of Z ;
take g = g9; :: thesis: S₁[f,g]
thus S₁[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 S₁[f,F . f] from FUNCT_2:sch 3(A10);
Z c= F .: (Funcs ((F₁() /\ F₃()),(F₂() /\ F₄())))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Z or y in F .: (Funcs ((F₁() /\ F₃()),(F₂() /\ F₄()))) )
assume y in Z ; :: thesis: y in F .: (Funcs ((F₁() /\ F₃()),(F₂() /\ F₄())))
then consider phi being Element of Funcs (F₁(),F₂()) such that
A14: y = F₅(phi) and
A15: phi .: F₃() c= F₄() ;
rng (phi | F₃()) c= F₄() by A15, RELAT_1:115;
then A16: rng (phi | F₃()) c= F₂() /\ F₄() by XBOOLE_1:19;
A17: dom (phi | F₃()) = (dom phi) /\ F₃() by RELAT_1:61
.= F₁() /\ F₃() by FUNCT_2:def 1 ;
then reconsider x = phi | F₃() as Element of Funcs ((F₁() /\ F₃()),(F₂() /\ F₄())) by A16, FUNCT_2:def 2;
phi | F₃() in Funcs ((F₁() /\ F₃()),(F₂() /\ F₄())) by A17, A16, FUNCT_2:def 2;
then A18: x in dom F by FUNCT_2:def 1;
y = F . x by A13, A14;
hence y in F .: (Funcs ((F₁() /\ F₃()),(F₂() /\ F₄()))) by A18, FUNCT_1:def 6; :: thesis: verum

end;

hence contradiction by A1, A2, A5; :: thesis: verum