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

proof

thus for v being set st v in supp M holds
v in I :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: I c= supp M

proof

let v be set ; :: thesis: ( v in supp M implies v in I )
assume v in supp M ; :: thesis: v in I
then v in { x where x is Element of I : M . x <> {} } by Def3;
then consider x being Element of I such that
A2: v = x and
M . x <> {} ;
thus v in I by A2; :: thesis: verum

end;

thus for v being set st v in I holds
v in supp M :: according to TARSKI:def 3 :: thesis: verum

proof

let v be set ; :: thesis: ( v in I implies v in supp M )
assume A3: v in I ; :: thesis: v in supp M
then M . v <> {} ;
then v in { x where x is Element of I : M . x <> {} } by A3;
hence v in supp M by Def3; :: thesis: verum

end;

end;

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