per cases ( F₂() = {} or F₁() = {} or ( F₁() <> {} & F₂() <> {} ) ) ;

suppose A2: F₂() = {} ; :: thesis: ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
P₁[x,f . x]

A3: now

let x be set ; :: thesis: not x in F₁()
assume x in F₁() ; :: thesis: contradiction
then ex y being set st
( y in F₂() & P₁[x,y] ) by A1;
hence contradiction by A2; :: thesis: verum

end;

consider f being Function of F₁(),F₂();
take f ; :: thesis: for x being set st x in F₁() holds
P₁[x,f . x]
thus for x being set st x in F₁() holds
P₁[x,f . x] by A3; :: thesis: verum

end;

suppose A4: F₁() = {} ; :: thesis: ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
P₁[x,f . x]

consider f being Function of F₁(),F₂();
take f ; :: thesis: for x being set st x in F₁() holds
P₁[x,f . x]
thus for x being set st x in F₁() holds
P₁[x,f . x] by A4; :: thesis: verum

end;

suppose ( F₁() <> {} & F₂() <> {} ) ; :: thesis: ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
P₁[x,f . x]

then reconsider X = F₁(), Y = F₂() as non empty set ;
set M = { { ff where ff is Element of Y : P₁[tt,ff] } where tt is Element of X : verum } ;
consider x0 being Element of X;
{ ff where ff is Element of Y : P₁[x0,ff] } in { { ff where ff is Element of Y : P₁[tt,ff] } where tt is Element of X : verum } ;
then reconsider M = { { ff where ff is Element of Y : P₁[tt,ff] } where tt is Element of X : verum } as non empty set ;

now

let x be set ; :: thesis: ( x in M implies x <> {} )
assume x in M ; :: thesis: x <> {}
then consider t being Element of X such that
A5: x = { ff where ff is Element of Y : P₁[t,ff] } ;
consider ff being set such that
A6: ff in Y and
A7: P₁[t,ff] by A1;
ff in x by A5, A6, A7;
hence x <> {} ; :: thesis: verum

end;

then consider C being Function such that
dom C = M and
A8: for x being set st x in M holds
C . x in x by WELLORD2:28;
deffunc H₁( set ) -> set = C . { ff where ff is Element of Y : P₁[$1,ff] } ;
consider f being Function such that
A9: dom f = X and
A10: for x being set st x in X holds
f . x = H₁(x) from FUNCT_1:sch 3();
rng f c= Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Y )
assume x in rng f ; :: thesis: x in Y
then consider y being set such that
A11: y in X and
A12: x = f . y by A9, FUNCT_1:def 5;
set y0 = { ff where ff is Element of Y : P₁[y,ff] } ;
A13: x = C . { ff where ff is Element of Y : P₁[y,ff] } by A10, A11, A12;
{ ff where ff is Element of Y : P₁[y,ff] } in M by A11;
then x in { ff where ff is Element of Y : P₁[y,ff] } by A8, A13;
then ex ff being Element of Y st
( x = ff & P₁[y,ff] ) ;
hence x in Y ; :: thesis: verum

end;

then reconsider f = f as Function of F₁(),F₂() by A9, Def1, RELSET_1:11;
take f ; :: thesis: for x being set st x in F₁() holds
P₁[x,f . x]
let x be set ; :: thesis: ( x in F₁() implies P₁[x,f . x] )
set x0 = { ff where ff is Element of Y : P₁[x,ff] } ;
assume A14: x in F₁() ; :: thesis: P₁[x,f . x]
then A15: { ff where ff is Element of Y : P₁[x,ff] } in M ;
f . x = C . { ff where ff is Element of Y : P₁[x,ff] } by A10, A14;
then f . x in { ff where ff is Element of Y : P₁[x,ff] } by A8, A15;
then ex ff being Element of Y st
( ff = f . x & P₁[x,ff] ) ;
hence P₁[x,f . x] ; :: thesis: verum

end;

end;