let s be State of SCMPDS; :: thesis: for iloc being Nat
for a being Int_position holds s . a = (s +* (Start-At (iloc,SCMPDS))) . a
let iloc be Nat; :: thesis: for a being Int_position holds s . a = (s +* (Start-At (iloc,SCMPDS))) . a
let a be Int_position; :: thesis: s . a = (s +* (Start-At (iloc,SCMPDS))) . a
a in the carrier of SCMPDS ;
then a in dom s by PARTFUN1:def 2;
then A1: ( dom (Start-At (iloc,SCMPDS)) = {(IC )} & a in (dom s) \/ (dom (Start-At (iloc,SCMPDS))) ) by XBOOLE_0:def 3;
a <> IC by SCMPDS_2:43;
then not a in {(IC )} by TARSKI:def 1;
hence s . a = (s +* (Start-At (iloc,SCMPDS))) . a by A1, FUNCT_4:def 1; :: thesis: verum