consider f being Function such that
A2: dom f = F₁() and
A3: for i being object st i in F₁() holds
P₁[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
P₁[i,f . i]
thus for i being object st i in F₁() holds
P₁[i,f . i] by A3; :: thesis: verum