theorem Th3: :: SCMFSA_M:3

for p being PartState of SCM+FSA holds dom (Initialized p) = ((dom p) \/ {(intloc 0)}) \/ {(IC )}