A2: now :: thesis: ( F₂() = {} implies not F₁() <> {} )

set x = the Element of F₁();
assume A3: F₂() = {} ; :: thesis: not F₁() <> {}
assume A4: F₁() <> {} ; :: thesis: contradiction
then ( P₁[ the Element of F₁()] implies F₃( the Element of F₁()) in F₂() ) by A1;
hence contradiction by A1, A3, A4; :: thesis: verum

end;

consider f being Function such that
A5: dom f = F₁() and
A6: for x being set st x in F₁() holds
( ( P₁[x] implies f . x = F₃(x) ) & ( P₁[x] implies f . x = F₄(x) ) ) from PARTFUN1:sch 1();
rng f c= F₂()

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in F₂() )
assume y in rng f ; :: thesis: y in F₂()
then consider x being set such that
A7: x in dom f and
A8: y = f . x by FUNCT_1:def 3;
A9: ( P₁[x] implies f . x = F₄(x) ) by A5, A6, A7;
( P₁[x] implies f . x = F₃(x) ) by A5, A6, A7;
hence y in F₂() by A1, A5, A7, A8, A9; :: thesis: verum

end;

then f is Function of F₁(),F₂() by A5, A2, Def1, RELSET_1:4;
hence ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
( ( P₁[x] implies f . x = F₃(x) ) & ( P₁[x] implies f . x = F₄(x) ) ) by A6; :: thesis: verum