A2: for x being object st x in F₁() holds
ex y being object st
( y in F₂() & P₁[x,y] )

proof

let x be object ; :: thesis: ( x in F₁() implies ex y being object st
( y in F₂() & P₁[x,y] ) )
assume x in F₁() ; :: thesis: ex y being object st
( y in F₂() & P₁[x,y] )
then consider y being Element of F₂() such that
A3: P₁[x,y] by A1;
take y ; :: thesis: ( y in F₂() & P₁[x,y] )
thus ( y in F₂() & P₁[x,y] ) by A3; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = F₁() & rng f c= F₂() & ( for x being object st x in F₁() holds
P₁[x,f . x] ) ) from FUNCT_1:sch 6(A2);
reconsider f = f as Function of F₁(),F₂() by A4, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: for x being object st x in F₁() holds
P₁[x,f . x]
thus for x being object st x in F₁() holds
P₁[x,f . x] by A4; :: thesis: verum