let s1, s2 be State of SCMPDS; :: thesis: ( IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) implies s1 = s2 )

assume that

A1: IC s1 = IC s2 and

A2: for a being Int_position holds s1 . a = s2 . a ; :: thesis: s1 = s2

A3: the carrier of SCMPDS = {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4

.= {(IC )} \/ SCM-Data-Loc ;

A4: dom (s2 | (dom s2)) = (dom s2) /\ (dom s2) by RELAT_1:61

.= dom s2

.= {(IC )} \/ SCM-Data-Loc by A3, PARTFUN1:def 2 ;

A5: dom (s1 | (dom s1)) = (dom s1) /\ (dom s1) by RELAT_1:61

.= dom s1

.= {(IC )} \/ SCM-Data-Loc by A3, PARTFUN1:def 2 ;

A6: ( s1 | (dom s1) = s1 & s2 | (dom s2) = s2 ) by RELAT_1:69;

assume that

A1: IC s1 = IC s2 and

A2: for a being Int_position holds s1 . a = s2 . a ; :: thesis: s1 = s2

A3: the carrier of SCMPDS = {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4

.= {(IC )} \/ SCM-Data-Loc ;

A4: dom (s2 | (dom s2)) = (dom s2) /\ (dom s2) by RELAT_1:61

.= dom s2

.= {(IC )} \/ SCM-Data-Loc by A3, PARTFUN1:def 2 ;

A5: dom (s1 | (dom s1)) = (dom s1) /\ (dom s1) by RELAT_1:61

.= dom s1

.= {(IC )} \/ SCM-Data-Loc by A3, PARTFUN1:def 2 ;

A6: ( s1 | (dom s1) = s1 & s2 | (dom s2) = s2 ) by RELAT_1:69;

now :: thesis: for x being object st x in {(IC )} \/ SCM-Data-Loc holds

(s1 | (dom s1)) . x = (s2 | (dom s2)) . x

hence
s1 = s2
by A6, A5, A4, FUNCT_1:2; :: thesis: verum(s1 | (dom s1)) . x = (s2 | (dom s2)) . x

let x be object ; :: thesis: ( x in {(IC )} \/ SCM-Data-Loc implies (s1 | (dom s1)) . b_{1} = (s2 | (dom s2)) . b_{1} )

assume A7: x in {(IC )} \/ SCM-Data-Loc ; :: thesis: (s1 | (dom s1)) . b_{1} = (s2 | (dom s2)) . b_{1}

end;assume A7: x in {(IC )} \/ SCM-Data-Loc ; :: thesis: (s1 | (dom s1)) . b

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

end;

suppose
x in {(IC )}
; :: thesis: (s1 | (dom s1)) . b_{1} = (s2 | (dom s2)) . b_{1}

then A8:
x = IC
by TARSKI:def 1;

hence (s1 | (dom s1)) . x = IC s1 by A5, A7, FUNCT_1:47

.= (s2 | (dom s2)) . x by A1, A4, A7, A8, FUNCT_1:47 ;

:: thesis: verum

end;hence (s1 | (dom s1)) . x = IC s1 by A5, A7, FUNCT_1:47

.= (s2 | (dom s2)) . x by A1, A4, A7, A8, FUNCT_1:47 ;

:: thesis: verum

suppose
x in SCM-Data-Loc
; :: thesis: (s1 | (dom s1)) . b_{1} = (s2 | (dom s2)) . b_{1}

then A9:
x is Int_position
by AMI_2:def 16;

thus (s1 | (dom s1)) . x = s1 . x by A5, A7, FUNCT_1:47

.= s2 . x by A2, A9

.= (s2 | (dom s2)) . x by A4, A7, FUNCT_1:47 ; :: thesis: verum

end;thus (s1 | (dom s1)) . x = s1 . x by A5, A7, FUNCT_1:47

.= s2 . x by A2, A9

.= (s2 | (dom s2)) . x by A4, A7, FUNCT_1:47 ; :: thesis: verum