defpred S₁[ object , object ] means ( $1 in F₁() & $2 in F₂() & P₁[$1,$2] );
A2: for x being object st x in F₁() holds
ex y being object st
( y in F₂() & S₁[x,y] )

proof

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

end;

consider f being Function of F₁(),F₂() such that
A4: for x being object st x in F₁() holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
take f ; :: thesis: for x being Element of F₁() holds P₁[x,f . x]
let x be Element of F₁(); :: thesis: P₁[x,f . x]
thus P₁[x,f . x] by A4; :: thesis: verum