let R be good 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 ) & ( for i being Element of NAT holds s1 . i = s2 . i ) 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 ) & ( for i being Element of NAT holds s1 . i = s2 . i ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Data-Location of R holds s1 . a = s2 . a and
A3: for i being Element of NAT holds s1 . i = s2 . i ; :: thesis: s1 = s2
A5: dom s1 = the carrier of (SCM R) by PARTFUN1:def 4;
A7: dom s2 = the carrier of (SCM R) by PARTFUN1:def 4;

A8: now

A9: SCM-Memory = ({(IC (SCM R))} \/ (Data-Locations SCM)) \/ NAT by AMI_3:72, SCMRING2:def 1;
let x be set ; :: thesis: ( x in SCM-Memory implies s1 . b₁ = s2 . b₁ )
assume x in SCM-Memory ; :: thesis: s1 . b₁ = s2 . b₁
then A10: ( x in {(IC (SCM R))} \/ (Data-Locations SCM) or x in NAT ) by A9, XBOOLE_0:def 3;

per cases ( x in {(IC (SCM R))} or x in Data-Locations SCM or x in NAT ) by A10, XBOOLE_0:def 3;

suppose x in {(IC (SCM R))} ; :: thesis: s1 . b₁ = s2 . b₁

then x = IC (SCM R) by TARSKI:def 1;
hence s1 . x = s2 . x by A1; :: thesis: verum

end;

suppose x in Data-Locations SCM ; :: thesis: s1 . b₁ = s2 . b₁

then x is Data-Location of R by SCMRING2:1;
hence s1 . x = s2 . x by A2; :: thesis: verum

end;

suppose x in NAT ; :: thesis: s1 . b₁ = s2 . b₁

then reconsider l = x as Element of NAT ;
l = x ;
hence s1 . x = s2 . x by A3; :: thesis: verum

end;

end;

end;

SCM-Memory = dom s1 by A5, SCMRING2:def 1;
hence s1 = s2 by A5, A7, A8, FUNCT_1:9; :: thesis: verum