theorem Th47: :: SCMFSA_2:54

for A being Data-Location
for a being Int-Location
for S being State of SCM
for s, s1 being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a