theorem :: SCMFSA_M:5

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