defpred S₁[ object , object ] means $2 = F₃($1);
A2: for x being object st x in F₁() holds
ex y being object st
( y in F₂() & S₁[x,y] ) by A1;
consider f being Function of F₁(),F₂() such that
A3: 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 set st x in F₁() holds
f . x = F₃(x)
let x be set ; :: thesis: ( x in F₁() implies f . x = F₃(x) )
thus ( x in F₁() implies f . x = F₃(x) ) by A3; :: thesis: verum