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