A2:
for e being object st e in F_{2}() holds

ex u being object st

( u in F_{3}() & P_{1}[e,u] )

A5: ( dom f = F_{2}() & rng f c= F_{3}() )
and

A6: for e being object st e in F_{2}() holds

P_{1}[e,f . e]
from FUNCT_1:sch 6(A2);

reconsider f = f as Function of F_{2}(),F_{3}() by A5, FUNCT_2:def 1, RELSET_1:4;

take f ; :: thesis: for e being Element of F_{1}() st e in F_{2}() holds

ex u being Element of F_{1}() st

( u in F_{3}() & u = f . e & P_{1}[e,u] )

for e being Element of F_{1}() st e in F_{2}() holds

ex u being Element of F_{1}() st

( u in F_{3}() & u = f . e & P_{1}[e,u] )
_{1}() st e in F_{2}() holds

ex u being Element of F_{1}() st

( u in F_{3}() & u = f . e & P_{1}[e,u] )
; :: thesis: verum

ex u being object st

( u in F

proof

consider f being Function such that
let e be object ; :: thesis: ( e in F_{2}() implies ex u being object st

( u in F_{3}() & P_{1}[e,u] ) )

assume A3: e in F_{2}()
; :: thesis: ex u being object st

( u in F_{3}() & P_{1}[e,u] )

then reconsider e1 = e as Element of F_{2}() ;

reconsider e1 = e1 as Element of F_{1}() by A3;

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

A4: ( u in F_{3}() & P_{1}[e1,u] )
by A1, A3;

reconsider u1 = u as set ;

take u1 ; :: thesis: ( u1 in F_{3}() & P_{1}[e,u1] )

thus ( u1 in F_{3}() & P_{1}[e,u1] )
by A4; :: thesis: verum

end;( u in F

assume A3: e in F

( u in F

then reconsider e1 = e as Element of F

reconsider e1 = e1 as Element of F

consider u being Element of F

A4: ( u in F

reconsider u1 = u as set ;

take u1 ; :: thesis: ( u1 in F

thus ( u1 in F

A5: ( dom f = F

A6: for e being object st e in F

P

reconsider f = f as Function of F

take f ; :: thesis: for e being Element of F

ex u being Element of F

( u in F

for e being Element of F

ex u being Element of F

( u in F

proof

hence
for e being Element of F
let e be Element of F_{1}(); :: thesis: ( e in F_{2}() implies ex u being Element of F_{1}() st

( u in F_{3}() & u = f . e & P_{1}[e,u] ) )

assume A7: e in F_{2}()
; :: thesis: ex u being Element of F_{1}() st

( u in F_{3}() & u = f . e & P_{1}[e,u] )

then reconsider e1 = f . e as Element of F_{3}() by FUNCT_2:5;

reconsider fe = e1 as Element of F_{1}() ;

take fe ; :: thesis: ( fe in F_{3}() & fe = f . e & P_{1}[e,fe] )

thus ( fe in F_{3}() & fe = f . e & P_{1}[e,fe] )
by A6, A7; :: thesis: verum

end;( u in F

assume A7: e in F

( u in F

then reconsider e1 = f . e as Element of F

reconsider fe = e1 as Element of F

take fe ; :: thesis: ( fe in F

thus ( fe in F

ex u being Element of F

( u in F