consider f being Function such that
A1: dom f = F₁() and
A2: for i being object st i in F₁() holds
f . i = F₂(i) from FUNCT_1:sch 3();
reconsider f = f as ManySortedSet of F₁() by A1, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: for i being set st i in F₁() holds
f . i = F₂(i)
thus for i being set st i in F₁() holds
f . i = F₂(i) by A2; :: thesis: verum