let a be Int_position ; :: thesis: for s being State of SCMPDS holds (Dstate s) . a = s . a
let s be State of SCMPDS ; :: thesis: (Dstate s) . a = s . a
( a in SCM-Data-Loc implies (Dstate s) . a = s . a ) by Def1;
hence (Dstate s) . a = s . a by SCMPDS_2:def 2; :: thesis: verum