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]

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

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;

hence for x being set st x in F₁() holds
P₁[x,f . x] ; :: thesis: verum

end;

suppose A3: 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 A3; :: 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
A4: x = { ff where ff is Element of Y : P₁[t,ff] } ;
consider ff being set such that
A5: ( ff in Y & P₁[t,ff] ) by A1;
ff in x by A4, A5;
hence x <> {} ; :: thesis: verum

end;

then consider C being Function such that
dom C = M and
A6: 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
A7: dom f = X and
A8: 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
A9: ( y in X & x = f . y ) by A7, FUNCT_1:def 5;
set y0 = { ff where ff is Element of Y : P₁[y,ff] } ;
( x = C . { ff where ff is Element of Y : P₁[y,ff] } & { ff where ff is Element of Y : P₁[y,ff] } in M ) by A8, A9;
then x in { ff where ff is Element of Y : P₁[y,ff] } by A6;
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 A7, 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 A10: x in F₁() ; :: thesis: P₁[x,f . x]
then A11: { 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 A8, A10;
then f . x in { ff where ff is Element of Y : P₁[x,ff] } by A6, A11;
then ex ff being Element of Y st
( ff = f . x & P₁[x,ff] ) ;
hence P₁[x,f . x] ; :: thesis: verum

end;

end;