for s being State of SCM+FSA holds FinSeq-Locations c= dom s