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