let R be non trivial Ring; :: thesis: for s1, s2 being State of (SCM R) st IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) holds

s1 = s2

let s1, s2 be State of (SCM R); :: thesis: ( IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) implies s1 = s2 )

assume A1: IC s1 = IC s2 ; :: thesis: ( ex a being Data-Location of R st not s1 . a = s2 . a or s1 = s2 )

( IC in dom s1 & IC in dom s2 ) by MEMSTR_0:2;

then A2: ( s1 = (DataPart s1) +* (Start-At ((IC s1),(SCM R))) & s2 = (DataPart s2) +* (Start-At ((IC s2),(SCM R))) ) by MEMSTR_0:26;

assume A3: for a being Data-Location of R holds s1 . a = s2 . a ; :: thesis: s1 = s2

DataPart s1 = DataPart s2

s1 = s2

let s1, s2 be State of (SCM R); :: thesis: ( IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) implies s1 = s2 )

assume A1: IC s1 = IC s2 ; :: thesis: ( ex a being Data-Location of R st not s1 . a = s2 . a or s1 = s2 )

( IC in dom s1 & IC in dom s2 ) by MEMSTR_0:2;

then A2: ( s1 = (DataPart s1) +* (Start-At ((IC s1),(SCM R))) & s2 = (DataPart s2) +* (Start-At ((IC s2),(SCM R))) ) by MEMSTR_0:26;

assume A3: for a being Data-Location of R holds s1 . a = s2 . a ; :: thesis: s1 = s2

DataPart s1 = DataPart s2

proof

hence
s1 = s2
by A1, A2; :: thesis: verum
A4:
dom (DataPart s1) = Data-Locations
by MEMSTR_0:9;

hence dom (DataPart s1) = dom (DataPart s2) by MEMSTR_0:9; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom (DataPart s1) or (DataPart s1) . b_{1} = (DataPart s2) . b_{1} )

let x be object ; :: thesis: ( not x in dom (DataPart s1) or (DataPart s1) . x = (DataPart s2) . x )

assume A5: x in dom (DataPart s1) ; :: thesis: (DataPart s1) . x = (DataPart s2) . x

then A6: x is Data-Location of R by A4, SCMRING2:23;

thus (DataPart s1) . x = s1 . x by A5, A4, FUNCT_1:49

.= s2 . x by A6, A3

.= (DataPart s2) . x by A5, A4, FUNCT_1:49 ; :: thesis: verum

end;hence dom (DataPart s1) = dom (DataPart s2) by MEMSTR_0:9; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom (DataPart s1) or (DataPart s1) . x = (DataPart s2) . x )

assume A5: x in dom (DataPart s1) ; :: thesis: (DataPart s1) . x = (DataPart s2) . x

then A6: x is Data-Location of R by A4, SCMRING2:23;

thus (DataPart s1) . x = s1 . x by A5, A4, FUNCT_1:49

.= s2 . x by A6, A3

.= (DataPart s2) . x by A5, A4, FUNCT_1:49 ; :: thesis: verum