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

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