let I be non empty set ; :: thesis: for M1, M2 being V8() ManySortedSet of st supp M1 = supp M2 & M1 | (supp M1) = M2 | (supp M2) holds
M1 = M2
let M1, M2 be V8() ManySortedSet of ; :: thesis: ( supp M1 = supp M2 & M1 | (supp M1) = M2 | (supp M2) implies M1 = M2 )
assume that
supp M1 = supp M2 and
A1: M1 | (supp M1) = M2 | (supp M2) ; :: thesis: M1 = M2
A2: ( dom M1 = I & dom M2 = I ) by PARTFUN1:def 4;
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 )
assume A3: 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 A3;
then A4: x in supp M1 by Def3;
not M2 . x is empty by A3;
then x in { a where a is Element of I : M2 . a <> {} } by A3;
then A5: x in supp M2 by Def3;
( dom (M1 | (supp M1)) = (dom M1) /\ (supp M1) & dom (M2 | (supp M2)) = (dom M2) /\ (supp M2) ) by RELAT_1:90;
then A6: ( x in dom (M1 | (supp M1)) & x in dom (M2 | (supp M2)) ) by A2, A3, A4, A5, XBOOLE_0:def 4;
then M1 . x = (M2 | (supp M2)) . x by A1, FUNCT_1:70
.= M2 . x by A6, FUNCT_1:70 ;
hence M1 . x = M2 . x ; :: thesis: verum

end;

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