set Z = { F₅(phi') where phi' is Element of Funcs F₁(),F₂() : phi' .: F₃() c= F₄() } ;
consider x being Element of { F₅(phi') where phi' is Element of Funcs F₁(),F₂() : phi' .: F₃() c= F₄() } ;
assume A4: not { F₅(phi') where phi' is Element of Funcs F₁(),F₂() : phi' .: F₃() c= F₄() } is finite ; :: thesis: contradiction
then { F₅(phi') where phi' is Element of Funcs F₁(),F₂() : phi' .: F₃() c= F₄() } <> {} ;
then x in { F₅(phi') where phi' is Element of Funcs F₁(),F₂() : phi' .: F₃() c= F₄() } ;
then consider phi being Element of Funcs F₁(),F₂() such that
x = F₅(phi) and
A5: phi .: F₃() c= F₄() ;

now

A6: ( F₁() = dom phi & rng phi c= F₂() ) by FUNCT_2:def 1;
assume F₂() /\ F₄() = {} ; :: thesis: F₁() /\ F₃() = {}
then phi .: F₃() = {} by A5, XBOOLE_1:3, XBOOLE_1:19;
then F₁() misses F₃() by A6, RELAT_1:151;
hence F₁() /\ F₃() = {} by XBOOLE_0:def 7; :: thesis: verum

end;

then reconsider FF = Funcs (F₁() /\ F₃()),(F₂() /\ F₄()), Z = { F₅(phi') where phi' is Element of Funcs F₁(),F₂() : phi' .: F₃() c= F₄() } as non empty set by A4, FUNCT_2:11;
A7: ( F₁() /\ F₃() c= F₁() & F₂() /\ F₄() c= F₂() ) by XBOOLE_1:17;
A8: F₂() /\ F₄() c= F₄() by XBOOLE_1:17;
defpred S₁[ set , set ] means for phi being Element of Funcs F₁(),F₂() st phi | F₃() = $1 holds
$2 = F₅(phi);

A9: now

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
A10: phi | (F₁() /\ F₃()) = f by A7, Th14;
A11: phi | F₃() = f by A10, Th15;
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, A11, XBOOLE_1:1;
then phi .: F₃() c= F₄() by RELAT_1:148;
then F₅(phi) in Z ;
then reconsider g' = F₅(phi) as Element of Z ;
take g = g'; :: thesis: S₁[f,g]
thus S₁[f,g] by A3, A11; :: thesis: verum

end;

consider F being Function of FF,Z such that
A12: for f being Element of FF holds S₁[f,F . f] from FUNCT_2:sch 3(A9);
Z c= F .: (Funcs (F₁() /\ F₃()),(F₂() /\ F₄()))

proof

let y be set ; :: 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
A13: y = F₅(phi) and
A14: phi .: F₃() c= F₄() ;
A15: dom (phi | F₃()) = (dom phi) /\ F₃() by RELAT_1:90
.= F₁() /\ F₃() by FUNCT_2:def 1 ;
rng (phi | F₃()) c= F₄() by A14, RELAT_1:148;
then A16: rng (phi | F₃()) c= F₂() /\ F₄() by XBOOLE_1:19;
then A17: phi | F₃() in Funcs (F₁() /\ F₃()),(F₂() /\ F₄()) by A15, FUNCT_2:def 2;
reconsider x = phi | F₃() as Element of Funcs (F₁() /\ F₃()),(F₂() /\ F₄()) by A15, A16, FUNCT_2:def 2;
A18: x in dom F by A17, FUNCT_2:def 1;
y = F . x by A12, A13;
hence y in F .: (Funcs (F₁() /\ F₃()),(F₂() /\ F₄())) by A18, FUNCT_1:def 12; :: thesis: verum

end;

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