let I be non empty set ; :: thesis: for M being V8() ManySortedSet of I holds M = ([0] I) +* (M | (supp M))
let M be V8() ManySortedSet of I; :: thesis: M = ([0] I) +* (M | (supp M))
set MM = M | (supp M);
A1: I c= supp M

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in I or v in supp M )
assume A2: v in I ; :: thesis: v in supp M
then M . v <> {} ;
then v in { x where x is Element of I : M . x <> {} } by A2;
hence v in supp M by Def3; :: thesis: verum

end;

dom M = I by PARTFUN1:def 4;
then M | (supp M) = M by A1, RELAT_1:97;
hence M = ([0] I) +* (M | (supp M)) by Th1; :: thesis: verum