let I be set ; :: thesis: for M being ManySortedSet of I holds M * (id I) = M
let M be ManySortedSet of I; :: thesis: M * (id I) = M
I = dom M by PARTFUN1:def 2;
hence M * (id I) = M by RELAT_1:52; :: thesis: verum