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