let t1, t2 be State of SCMPDS; :: thesis: ( DataPart t1 = DataPart t2 implies Dstate t1 = Dstate t2 )
set s1 = Dstate t1;
set s2 = Dstate t2;

A1: now

let i be Element of NAT ; :: thesis: (Dstate t1) . i = (Dstate t2) . i
thus (Dstate t1) . i = goto 0 by Def1
.= (Dstate t2) . i by Def1 ; :: thesis: verum

end;

assume A2: DataPart t1 = DataPart t2 ; :: thesis: Dstate t1 = Dstate t2

A3: now

let a be Int_position ; :: thesis: (Dstate t1) . a = (Dstate t2) . a
A4: a in SCM-Data-Loc by SCMPDS_2:def 2;
hence (Dstate t1) . a = t1 . a by Def1
.= t2 . a by A2, SCMPDS_3:4
.= (Dstate t2) . a by A4, Def1 ;
:: thesis: verum

end;

IC (Dstate t1) = 0 by Def1
.= IC (Dstate t2) by Def1 ;
hence Dstate t1 = Dstate t2 by A3, A1, SCMPDS_2:54; :: thesis: verum