let k1 be Integer; :: thesis: for a being Int_position
for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . (DataLoc (s1 . a),k1) = s2 . (DataLoc (s2 . a),k1)
let a be Int_position ; :: thesis: for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . (DataLoc (s1 . a),k1) = s2 . (DataLoc (s2 . a),k1)
let s1, s2 be State of SCMPDS ; :: thesis: ( DataPart s1 = DataPart s2 implies s1 . (DataLoc (s1 . a),k1) = s2 . (DataLoc (s2 . a),k1) )
assume A1: DataPart s1 = DataPart s2 ; :: thesis: s1 . (DataLoc (s1 . a),k1) = s2 . (DataLoc (s2 . a),k1)
A2: a in SCM-Data-Loc by SCMPDS_2:def 2;
then A3: s1 . a = (DataPart s1) . a by FUNCT_1:72, SCMPDS_2:100
.= s2 . a by A1, A2, FUNCT_1:72, SCMPDS_2:100 ;
A4: DataLoc (s1 . a),k1 in SCM-Data-Loc by SCMPDS_2:def 2;
hence s1 . (DataLoc (s1 . a),k1) = (DataPart s1) . (DataLoc (s1 . a),k1) by FUNCT_1:72, SCMPDS_2:100
.= s2 . (DataLoc (s2 . a),k1) by A1, A4, A3, FUNCT_1:72, SCMPDS_2:100 ;
:: thesis: verum