let a be Int_position ; :: thesis: for s being State of SCMPDS
for l being Element of NAT
for I being Program of SCMPDS holds (s +* (I +* (Start-At l,SCMPDS ))) . a = s . a
let s be State of SCMPDS ; :: thesis: for l being Element of NAT
for I being Program of SCMPDS holds (s +* (I +* (Start-At l,SCMPDS ))) . a = s . a
let l be Element of NAT ; :: thesis: for I being Program of SCMPDS holds (s +* (I +* (Start-At l,SCMPDS ))) . a = s . a
let I be Program of SCMPDS ; :: thesis: (s +* (I +* (Start-At l,SCMPDS ))) . a = s . a
not a in dom (I +* (Start-At l,SCMPDS )) by SCMPDS_4:61;
hence (s +* (I +* (Start-At l,SCMPDS ))) . a = s . a by FUNCT_4:12; :: thesis: verum