set b = the Element of F_{2}();

set M = { { ff where ff is Element of F_{2}() : P_{1}[tt,ff] } where tt is Element of F_{1}() : tt in F_{3}() } ;

set f = the Function of F_{1}(),F_{2}();

assume A2: for ff being Function of F_{1}(),F_{2}() ex t being Element of F_{1}() st

( t in F_{3}() & P_{1}[t,ff . t] )
; :: thesis: contradiction

then consider t being Element of F_{1}() such that

A3: t in F_{3}()
and

P_{1}[t, the Function of F_{1}(),F_{2}() . t]
;

{ ff where ff is Element of F_{2}() : P_{1}[t,ff] } in { { ff where ff is Element of F_{2}() : P_{1}[tt,ff] } where tt is Element of F_{1}() : tt in F_{3}() }
by A3;

then reconsider M = { { ff where ff is Element of F_{2}() : P_{1}[tt,ff] } where tt is Element of F_{1}() : tt in F_{3}() } as non empty set ;

dom Choice = M and

A7: for X being set st X in M holds

Choice . X in X by FUNCT_1:111;

defpred S_{1}[ Element of F_{1}(), set ] means ( ( $1 in F_{3}() implies $2 = Choice . { ff where ff is Element of F_{2}() : P_{1}[$1,ff] } ) & ( $1 in F_{3}() or $2 = the Element of F_{2}() ) );

_{1}(),F_{2}() such that

A10: for x being Element of F_{1}() holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A8);

set M = { { ff where ff is Element of F

set f = the Function of F

assume A2: for ff being Function of F

( t in F

then consider t being Element of F

A3: t in F

P

{ ff where ff is Element of F

then reconsider M = { { ff where ff is Element of F

now :: thesis: for X being set st X in M holds

X <> {}

then consider Choice being Function such that X <> {}

let X be set ; :: thesis: ( X in M implies X <> {} )

assume X in M ; :: thesis: X <> {}

then consider t being Element of F_{1}() such that

A4: X = { ff where ff is Element of F_{2}() : P_{1}[t,ff] }
and

A5: t in F_{3}()
;

consider ff being Element of F_{2}() such that

A6: P_{1}[t,ff]
by A1, A5;

ff in X by A4, A6;

hence X <> {} ; :: thesis: verum

end;assume X in M ; :: thesis: X <> {}

then consider t being Element of F

A4: X = { ff where ff is Element of F

A5: t in F

consider ff being Element of F

A6: P

ff in X by A4, A6;

hence X <> {} ; :: thesis: verum

dom Choice = M and

A7: for X being set st X in M holds

Choice . X in X by FUNCT_1:111;

defpred S

A8: now :: thesis: for t being Element of F_{1}() ex y being Element of F_{2}() st S_{1}[t,y]

consider f being Function of Flet t be Element of F_{1}(); :: thesis: ex y being Element of F_{2}() st S_{1}[t,y]

_{3}() implies t in F_{3}() )
;

hence ex y being Element of F_{2}() st S_{1}[t,y]
by A9; :: thesis: verum

end;A9: now :: thesis: ( t in F_{3}() implies Choice . { ff where ff is Element of F_{2}() : P_{1}[t,ff] } is Element of F_{2}() )

( t in Fset s = { ff where ff is Element of F_{2}() : P_{1}[t,ff] } ;

assume t in F_{3}()
; :: thesis: Choice . { ff where ff is Element of F_{2}() : P_{1}[t,ff] } is Element of F_{2}()

then { ff where ff is Element of F_{2}() : P_{1}[t,ff] } in M
;

then Choice . { ff where ff is Element of F_{2}() : P_{1}[t,ff] } in { ff where ff is Element of F_{2}() : P_{1}[t,ff] }
by A7;

then ex ff being Element of F_{2}() st

( Choice . { ff where ff is Element of F_{2}() : P_{1}[t,ff] } = ff & P_{1}[t,ff] )
;

hence Choice . { ff where ff is Element of F_{2}() : P_{1}[t,ff] } is Element of F_{2}()
; :: thesis: verum

end;assume t in F

then { ff where ff is Element of F

then Choice . { ff where ff is Element of F

then ex ff being Element of F

( Choice . { ff where ff is Element of F

hence Choice . { ff where ff is Element of F

hence ex y being Element of F

A10: for x being Element of F

now :: thesis: for t being Element of F_{1}() st t in F_{3}() holds

P_{1}[t,f . t]

hence
contradiction
by A2; :: thesis: verumP

let t be Element of F_{1}(); :: thesis: ( t in F_{3}() implies P_{1}[t,f . t] )

assume A11: t in F_{3}()
; :: thesis: P_{1}[t,f . t]

then A12: { ff where ff is Element of F_{2}() : P_{1}[t,ff] } in M
;

f . t = Choice . { ff where ff is Element of F_{2}() : P_{1}[t,ff] }
by A10, A11;

then f . t in { ff where ff is Element of F_{2}() : P_{1}[t,ff] }
by A7, A12;

then ex ff being Element of F_{2}() st

( f . t = ff & P_{1}[t,ff] )
;

hence P_{1}[t,f . t]
; :: thesis: verum

end;assume A11: t in F

then A12: { ff where ff is Element of F

f . t = Choice . { ff where ff is Element of F

then f . t in { ff where ff is Element of F

then ex ff being Element of F

( f . t = ff & P

hence P