consider f being Function such that
A1: dom f = F₁() and
A2: for d being Element of F₁() holds f . d = F₂(d) from FUNCT_1:sch 4();
f is ManySortedSet of F₁() by A1, PARTFUN1:def 2, RELAT_1:def 18;
hence ex X being ManySortedSet of F₁() st
for d being Element of F₁() holds X . d = F₂(d) by A2; :: thesis: verum