defpred S₁[ set , set ] means for e being set holds
( e in $2 iff ( e in F₂() . $1 & P₁[$1,e] ) );

A1: now

let i be set ; :: thesis: ( i in F₁() implies ex u being set st S₁[i,u] )
assume i in F₁() ; :: thesis: ex u being set st S₁[i,u]
defpred S₂[ set ] means P₁[i,$1];
ex u being set st
for e being set holds
( e in u iff ( e in F₂() . i & S₂[e] ) ) from XBOOLE_0:sch 1();
hence ex u being set st S₁[i,u] ; :: thesis: verum

end;

consider f being Function such that
A2: dom f = F₁() and
A3: for i being set st i in F₁() holds
S₁[i,f . i] from CLASSES1:sch 1(A1);
f is ManySortedSet of F₁() by A2, PARTFUN1:def 4, RELAT_1:def 18;
hence ex X being ManySortedSet of F₁() st
for i being set st i in F₁() holds
for e being set holds
( e in X . i iff ( e in F₂() . i & P₁[i,e] ) ) by A3; :: thesis: verum