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 PBOOLE:def 3;
hence M * (id I) = M by RELAT_1:78; :: thesis: verum