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;
assume A1: DataPart t1 = DataPart t2 ; :: thesis: Dstate t1 = Dstate t2
A2: IC (Dstate t1) = inspos 0 by Def1
.= IC (Dstate t2) by Def1 ;

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 A1, SCMPDS_3:4
.= (Dstate t2) . a by A4, Def1 ;
:: thesis: verum

end;

now

let i be Instruction-Location of SCMPDS ; :: thesis: (Dstate t1) . i = (Dstate t2) . i
A5: i in NAT by AMI_1:def 4;
hence (Dstate t1) . i = goto 0 by Def1
.= (Dstate t2) . i by A5, Def1 ;
:: thesis: verum

end;

hence Dstate t1 = Dstate t2 by A2, A3, SCMPDS_2:54; :: thesis: verum