let I be non empty set ; :: thesis: for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds
M1 = M2
let M1, M2 be V8() ManySortedSet of I; :: thesis: ( M1 | (support M1) = M2 | (support M2) implies M1 = M2 )
A1: dom M1 = I by PARTFUN1:def 2;
A2: dom M2 = I by PARTFUN1:def 2;
assume A3: M1 | (support M1) = M2 | (support M2) ; :: thesis: M1 = M2
for x being object st x in I holds
M1 . x = M2 . x
proof
let x be object ; :: thesis: ( x in I implies M1 . x = M2 . x )
A4: dom (M2 | (support M2)) = (dom M2) /\ (support M2) by RELAT_1:61;
assume A5: x in I ; :: thesis: M1 . x = M2 . x
then not M1 . x is empty ;
then A6: x in support M1 by A5;
not M2 . x is empty by A5;
then x in support M2 by A5;
then A7: x in dom (M2 | (support M2)) by A2, A5, A4, XBOOLE_0:def 4;
dom (M1 | (support M1)) = (dom M1) /\ (support M1) by RELAT_1:61;
then x in dom (M1 | (support M1)) by A1, A5, A6, XBOOLE_0:def 4;
then M1 . x = (M2 | (support 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 ; :: thesis: verum