A2:
for x being object st x in F_{1}() holds

ex y being object st

( y in F_{2}() & P_{1}[x,y] )

A4: ( dom f = F_{1}() & rng f c= F_{2}() & ( for x being object st x in F_{1}() holds

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

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

take f ; :: thesis: for x being object st x in F_{1}() holds

P_{1}[x,f . x]

thus for x being object st x in F_{1}() holds

P_{1}[x,f . x]
by A4; :: thesis: verum

ex y being object st

( y in F

proof

consider f being Function such that
let x be object ; :: thesis: ( x in F_{1}() implies ex y being object st

( y in F_{2}() & P_{1}[x,y] ) )

assume x in F_{1}()
; :: thesis: ex y being object st

( y in F_{2}() & P_{1}[x,y] )

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

A3: P_{1}[x,y]
by A1;

take y ; :: thesis: ( y in F_{2}() & P_{1}[x,y] )

thus ( y in F_{2}() & P_{1}[x,y] )
by A3; :: thesis: verum

end;( y in F

assume x in F

( y in F

then consider y being Element of F

A3: P

take y ; :: thesis: ( y in F

thus ( y in F

A4: ( dom f = F

P

reconsider f = f as Function of F

take f ; :: thesis: for x being object st x in F

P

thus for x being object st x in F

P