defpred S₁[ object , object ] means ex D1 being set st
( D1 = $1 & $2 = F₃(D1) );
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] )
reconsider x = x as set by TARSKI:1;
F₃(x) in F₂() by A3, A1;
hence ex y being object st
( y in F₂() & S₁[x,y] ) ; :: 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 set st x in F₁() holds
f . x = F₃(x)
let x be set ; :: thesis: ( x in F₁() implies f . x = F₃(x) )
assume x in F₁() ; :: thesis: f . x = F₃(x)
then S₁[x,f . x] by A4;
hence f . x = F₃(x) ; :: thesis: verum