theorem :: SCMFSA_2:48

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