theorem :: SCMFSA_2:47

for s being State of SCM+FSA holds dom (s | Int-Locations) = Int-Locations