let I be non empty set ; :: thesis: for M1, M2 being V8() ManySortedSet of I st M1 | (supp M1) = M2 | (supp M2) holds
M1 = M2
let M1, M2 be V8() ManySortedSet of I; :: thesis: ( M1 | (supp M1) = M2 | (supp M2) implies M1 = M2 )
A1: dom M1 = I by PARTFUN1:def 2;
A2: dom M2 = I by PARTFUN1:def 2;
assume A3: M1 | (supp M1) = M2 | (supp M2) ; :: thesis: M1 = M2
for x being set st x in I holds
M1 . x = M2 . x

proof

let x be set ; :: thesis: ( x in I implies M1 . x = M2 . x )
A4: dom (M2 | (supp M2)) = (dom M2) /\ (supp M2) by RELAT_1:61;
assume A5: x in I ; :: thesis: M1 . x = M2 . x
then not M1 . x is empty ;
then x in { a where a is Element of I : M1 . a <> {} } by A5;
then A6: x in supp M1 by Def3;
not M2 . x is empty by A5;
then x in { a where a is Element of I : M2 . a <> {} } by A5;
then x in supp M2 by Def3;
then A7: x in dom (M2 | (supp M2)) by A2, A5, A4, XBOOLE_0:def 4;
dom (M1 | (supp M1)) = (dom M1) /\ (supp M1) by RELAT_1:61;
then x in dom (M1 | (supp M1)) by A1, A5, A6, XBOOLE_0:def 4;
then M1 . x = (M2 | (supp M2)) . x by A3, FUNCT_1:47
.= M2 . x by A7, FUNCT_1:47 ;
hence M1 . x = M2 . x ; :: thesis: verum

end;

hence M1 = M2 by A1, A2, FUNCT_1:2; :: thesis: verum