let I be non empty set ; :: thesis: for M being non-empty ManySortedSet of I holds M = (EmptyMS I) +* (M | (support M))
let M be non-empty ManySortedSet of I; :: thesis: M = (EmptyMS I) +* (M | (support M))
set MM = M | (support M);
A1: I c= support M

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in I or v in support M )
assume A2: v in I ; :: thesis: v in support M
then M . v <> {} ;
hence v in support M by A2; :: thesis: verum

end;

dom M = I by PARTFUN1:def 2;
then M | (support M) = M by A1, RELAT_1:68;
hence M = (EmptyMS I) +* (M | (support M)) by Th1; :: thesis: verum