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 Instruction-Location of SCM R 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 Instruction-Location of SCM R 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 Instruction-Location of SCM R holds s1 . i = s2 . i ; :: thesis: s1 = s2
s1 is Element of product (SCM-OK R) by SCMRING2:def 1;
then consider g1 being Function such that
A4: ( s1 = g1 & dom g1 = dom (SCM-OK R) & ( for x being set st x in dom (SCM-OK R) holds
g1 . x in (SCM-OK R) . x ) ) by CARD_3:def 5;
s2 is Element of product (SCM-OK R) by SCMRING2:def 1;
then consider g2 being Function such that
A5: ( s2 = g2 & dom g2 = dom (SCM-OK R) & ( for x being set st x in dom (SCM-OK R) holds
g2 . x in (SCM-OK R) . x ) ) by CARD_3:def 5;
A6: ( SCM-Memory = dom g1 & SCM-Memory = dom g2 ) by A4, A5, FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in SCM-Memory implies g1 . b₁ = g2 . b₁ )
assume A7: x in SCM-Memory ; :: thesis: g1 . b₁ = g2 . b₁
SCM-Memory = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT by SCMRING2:def 1;
then A8: ( x in {(IC (SCM R))} \/ SCM-Data-Loc or x in NAT ) by A7, XBOOLE_0:def 3;

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

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

then x = IC (SCM R) by TARSKI:def 1;
hence g1 . x = g2 . x by A1, A4, A5; :: thesis: verum

end;

suppose x in SCM-Data-Loc ; :: thesis: g1 . b₁ = g2 . b₁

then x is Data-Location of R by SCMRING2:1;
hence g1 . x = g2 . x by A2, A4, A5; :: thesis: verum

end;

suppose x in NAT ; :: thesis: g1 . b₁ = g2 . b₁

then reconsider l = x as Instruction-Location of SCM R by AMI_1:def 4;
l = x ;
hence g1 . x = g2 . x by A3, A4, A5; :: thesis: verum

end;

end;

end;

hence s1 = s2 by A4, A5, A6, FUNCT_1:9; :: thesis: verum