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 AMI_2:def 16;
then A3: s1 . a = (DataPart s1) . a by FUNCT_1:49, SCMPDS_2:84
.= s2 . a by A1, A2, FUNCT_1:49, SCMPDS_2:84 ;
A4: DataLoc ((s1 . a),k1) in SCM-Data-Loc by AMI_2:def 16;
hence s1 . (DataLoc ((s1 . a),k1)) = (DataPart s1) . (DataLoc ((s1 . a),k1)) by FUNCT_1:49, SCMPDS_2:84
.= s2 . (DataLoc ((s2 . a),k1)) by A1, A4, A3, FUNCT_1:49, SCMPDS_2:84 ;
:: thesis: verum