let a be Int_position; :: thesis: for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . a = s2 . a
let s1, s2 be State of SCMPDS; :: thesis: ( DataPart s1 = DataPart s2 implies s1 . a = s2 . a )
assume A1: DataPart s1 = DataPart s2 ; :: thesis: s1 . a = s2 . a
A2: a in SCM-Data-Loc by AMI_2:def 16;
hence s1 . a = (DataPart s1) . a by FUNCT_1:49, SCMPDS_2:84
.= s2 . a by A1, A2, FUNCT_1:49, SCMPDS_2:84 ;
:: thesis: verum