theorem Th5: :: SCMRING4:5

for R being non trivial Ring
for a being Data-Location of R
for loc being Nat
for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a