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

let M be V8() ManySortedSet of I; :: thesis: M = (EmptyMS I) +* (M | (support M))

set MM = M | (support M);

A1: I c= support M

then M | (support M) = M by A1, RELAT_1:68;

hence M = (EmptyMS I) +* (M | (support M)) by Th1; :: thesis: verum

let M be V8() ManySortedSet of I; :: thesis: M = (EmptyMS I) +* (M | (support M))

set MM = M | (support M);

A1: I c= support M

proof

dom M = I
by PARTFUN1:def 2;
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;assume A2: v in I ; :: thesis: v in support M

then M . v <> {} ;

hence v in support M by A2; :: thesis: verum

then M | (support M) = M by A1, RELAT_1:68;

hence M = (EmptyMS I) +* (M | (support M)) by Th1; :: thesis: verum