theorem :: SCMFSA_M:37

for s being State of SCM+FSA holds
( ( for a being read-write Int-Location holds (Initialized s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) )