let s1, s2 be State of SCMPDS ; :: thesis: ( ( for a being Int_position holds s1 . a = s2 . a ) implies Dstate s1 = Dstate s2 )
assume for a being Int_position holds s1 . a = s2 . a ; :: thesis: Dstate s1 = Dstate s2
then DataPart s1 = DataPart s2 by SCMPDS_4:23;
hence Dstate s1 = Dstate s2 by SCMPDS_8:2; :: thesis: verum