theorem :: SCMFSA_M:21

for s being State of SCM+FSA
for a being Int-Location
for l being Nat holds (s +* (Start-At (l,SCM+FSA))) . a = s . a