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