defpred S₁[ object , object ] means $2 in F₃($1);
A2: for e being object st e in F₁() holds
ex u being object st
( u in F₂() & S₁[e,u] ) by A1, XBOOLE_0:3;
consider t being Function such that
A3: ( dom t = F₁() & rng t c= F₂() ) and
A4: for e being object st e in F₁() holds
S₁[e,t . e] from FUNCT_1:sch 6(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