theorem Th4: :: SCMFSA_M:4

for p being PartState of SCM+FSA holds intloc 0 in dom (Initialized p)