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

A2: now :: thesis: for e being object st e in F₁() holds
ex fe being object st S₁[e,fe]

let e be object ; :: thesis: ( e in F₁() implies ex fe being object st S₁[e,fe] )
set fe = the Element of F₂(e);
assume A3: e in F₁() ; :: thesis: ex fe being object st S₁[e,fe]
reconsider fe = the Element of F₂(e) as object ;
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 object 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 2, RELAT_1:def 18;
take f ; :: thesis: for e being object st e in F₁() holds
f . e in F₂(e)
thus for e being object st e in F₁() holds
f . e in F₂(e) by A5; :: thesis: verum