defpred S₁[ set , set ] means $2 in F₃($1);
A2: for e being set st e in F₁() holds
ex u being set st
( u in F₂() & S₁[e,u] )

proof

let e be set ; :: thesis: ( e in F₁() implies ex u being set st
( u in F₂() & S₁[e,u] ) )
assume e in F₁() ; :: thesis: ex u being set st
( u in F₂() & S₁[e,u] )
then F₂() meets F₃(e) by A1;
hence ex u being set st
( u in F₂() & S₁[e,u] ) by XBOOLE_0:3; :: thesis: verum

end;

consider t being Function such that
A3: ( dom t = F₁() & rng t c= F₂() ) and
A4: for e being set st e in F₁() holds
S₁[e,t . e] from FUNCT_1:sch 5(A2);
reconsider t = t as Function of F₁(),F₂() by A3, Def1, RELSET_1:4;
take t ; :: thesis: for a being Element of F₁() holds t . a in F₃(a)
let a be Element of F₁(); :: thesis: t . a in F₃(a)
thus t . a in F₃(a) by A4; :: thesis: verum