theorem :: SCMFSA_M:9

for p being PartState of SCM+FSA holds (Initialized p) . (intloc 0) = 1