for a being Int-Location
for s being State of SCM+FSA holds (Initialize s) . a = s . a