theorem :: SCMFSA_2:43

for f being FinSeq-Location
for s being State of SCM+FSA holds f in dom s