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

A1: now :: thesis: for i being object st i in F₁() holds
ex u being object st S₁[i,u]

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

end;

consider f being Function such that
A2: dom f = F₁() and
A3: for i being object st i in F₁() holds
S₁[i,f . i] from CLASSES1:sch 1(A1);
reconsider f = f as ManySortedSet of F₁() by A2, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: for i being object st i in F₁() holds
for e being object holds
( e in f . i iff ( e in F₂() . i & P₁[i,e] ) )
let i be object ; :: thesis: ( i in F₁() implies for e being object holds
( e in f . i iff ( e in F₂() . i & P₁[i,e] ) ) )
assume i in F₁() ; :: thesis: for e being object holds
( e in f . i iff ( e in F₂() . i & P₁[i,e] ) )
then S₁[i,f . i] by A3;
hence for e being object holds
( e in f . i iff ( e in F₂() . i & P₁[i,e] ) ) ; :: thesis: verum