let I, A be set ; :: thesis: for s, ss being ManySortedSet of I holds (ss +* (s | A)) | A = s | A
let s, ss be ManySortedSet of I; :: thesis: (ss +* (s | A)) | A = s | A
dom s = I by PARTFUN1:def 2
.= dom ss by PARTFUN1:def 2 ;
then A /\ (dom ss) c= A /\ (dom s) ;
hence (ss +* (s | A)) | A = s | A by FUNCT_4:88; :: thesis: verum