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;
now :: thesis: for x being object st x in {(IC )} \/ SCM-Data-Loc holds
(s1 | (dom s1)) . x = (s2 | (dom s2)) . x
let x be object ; :: thesis: ( x in {(IC )} \/ SCM-Data-Loc implies (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1 )
assume A7: x in {(IC )} \/ SCM-Data-Loc ; :: thesis: (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1
per cases ( x in {(IC )} or x in SCM-Data-Loc ) by A7, XBOOLE_0:def 3;
suppose x in {(IC )} ; :: thesis: (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1
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;
suppose x in SCM-Data-Loc ; :: thesis: (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1
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;
end;
end;
hence s1 = s2 by A6, A5, A4, FUNCT_1:2; :: thesis: verum