let I be non empty set ; :: thesis: for M, N being ManySortedSet of I holds M +* N = N
let M, N be ManySortedSet of I; :: thesis: M +* N = N
dom M = I by PARTFUN1:def 2
.= dom N by PARTFUN1:def 2 ;
hence M +* N = N by FUNCT_4:19; :: thesis: verum