defpred S₁[ set , set ] means $2 in F₂($1);

A2: now

let e be set ; :: thesis: ( e in F₁() implies ex fe being set st S₁[e,fe] )
consider fe being Element of F₂(e);
assume A3: e in F₁() ; :: thesis: ex fe being set st S₁[e,fe]
reconsider fe = fe as set ;
take fe = fe; :: thesis: S₁[e,fe]
F₂(e) <> {} by A1, A3;
hence S₁[e,fe] ; :: thesis: verum

end;

consider f being Function such that
A4: dom f = F₁() and
A5: for e being set st e in F₁() holds
S₁[e,f . e] from CLASSES1:sch 1(A2);
reconsider f = f as ManySortedSet of F₁() by A4, PARTFUN1:def 4, RELAT_1:def 18;
take f ; :: thesis: for e being set st e in F₁() holds
f . e in F₂(e)
thus for e being set st e in F₁() holds
f . e in F₂(e) by A5; :: thesis: verum