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 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 set st x in F₁() holds
P₁[x,f . x] ) ) from WELLORD2:sch 1(A2);
reconsider f = f as Function of F₁(),F₂() by A4, FUNCT_2:def 1, RELSET_1:11;
take f ; :: thesis: for x being set st x in F₁() holds
P₁[x,f . x]
thus for x being set st x in F₁() holds
P₁[x,f . x] by A4; :: thesis: verum