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

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

hence
M1 = M2
; :: thesis: verum
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;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