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

proof

let x be set ; :: thesis: ( x in F₁() implies ex y being set st
( y in F₂() & P₁[x,y] ) )
assume x in F₁() ; :: thesis: ex y being set st
( y in F₂() & P₁[x,y] )
then reconsider x = x as Element of F₁() ;
ex y being Element of F₂() st P₁[x,y] by A1;
hence ex y being set st
( y in F₂() & P₁[x,y] ) ; :: thesis: verum

end;

consider f being Function of F₁(),F₂() such that
A3: for x being set st x in F₁() holds
P₁[x,f . x] from FUNCT_2:sch 1(A2);
reconsider f = f as Function of F₁(),F₂() ;
take f ; :: thesis: for x being Element of F₁() holds P₁[x,f . x]
thus for x being Element of F₁() holds P₁[x,f . x] by A3; :: thesis: verum