set b = the Element of F₂();
set M = { { ff where ff is Element of F₂() : P₁[tt,ff] } where tt is Element of F₁() : tt in F₃() } ;
set f = the Function of F₁(),F₂();
assume A2: for ff being Function of F₁(),F₂() ex t being Element of F₁() st
( t in F₃() & P₁[t,ff . t] ) ; :: thesis: contradiction
then consider t being Element of F₁() such that
A3: t in F₃() and
P₁[t, the Function of F₁(),F₂() . t] ;
{ ff where ff is Element of F₂() : P₁[t,ff] } in { { ff where ff is Element of F₂() : P₁[tt,ff] } where tt is Element of F₁() : tt in F₃() } by A3;
then reconsider M = { { ff where ff is Element of F₂() : P₁[tt,ff] } where tt is Element of F₁() : tt in F₃() } as non empty set ;

now :: thesis: for X being set st X in M holds
X <> {}

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

end;

then consider Choice being Function such that
dom Choice = M and
A7: for X being set st X in M holds
Choice . X in X by FUNCT_1:111;
defpred S₁[ Element of F₁(), set ] means ( ( $1 in F₃() implies $2 = Choice . { ff where ff is Element of F₂() : P₁[$1,ff] } ) & ( $1 in F₃() or $2 = the Element of F₂() ) );

A8: now :: thesis: for t being Element of F₁() ex y being Element of F₂() st S₁[t,y]

let t be Element of F₁(); :: thesis: ex y being Element of F₂() st S₁[t,y]

A9: now :: thesis: ( t in F₃() implies Choice . { ff where ff is Element of F₂() : P₁[t,ff] } is Element of F₂() )

set s = { ff where ff is Element of F₂() : P₁[t,ff] } ;
assume t in F₃() ; :: thesis: Choice . { ff where ff is Element of F₂() : P₁[t,ff] } is Element of F₂()
then { ff where ff is Element of F₂() : P₁[t,ff] } in M ;
then Choice . { ff where ff is Element of F₂() : P₁[t,ff] } in { ff where ff is Element of F₂() : P₁[t,ff] } by A7;
then ex ff being Element of F₂() st
( Choice . { ff where ff is Element of F₂() : P₁[t,ff] } = ff & P₁[t,ff] ) ;
hence Choice . { ff where ff is Element of F₂() : P₁[t,ff] } is Element of F₂() ; :: thesis: verum

end;

( t in F₃() implies t in F₃() ) ;
hence ex y being Element of F₂() st S₁[t,y] by A9; :: thesis: verum

end;

consider f being Function of F₁(),F₂() such that
A10: for x being Element of F₁() holds S₁[x,f . x] from FUNCT_2:sch 3(A8);

now :: thesis: for t being Element of F₁() st t in F₃() holds
P₁[t,f . t]

let t be Element of F₁(); :: thesis: ( t in F₃() implies P₁[t,f . t] )
assume A11: t in F₃() ; :: thesis: P₁[t,f . t]
then A12: { ff where ff is Element of F₂() : P₁[t,ff] } in M ;
f . t = Choice . { ff where ff is Element of F₂() : P₁[t,ff] } by A10, A11;
then f . t in { ff where ff is Element of F₂() : P₁[t,ff] } by A7, A12;
then ex ff being Element of F₂() st
( f . t = ff & P₁[t,ff] ) ;
hence P₁[t,f . t] ; :: thesis: verum

end;

hence contradiction by A2; :: thesis: verum