let s be State of SCM+FSA; :: thesis: dom (s | FinSeq-Locations) = FinSeq-Locations
FinSeq-Locations c= dom s by Th39;
hence dom (s | FinSeq-Locations) = FinSeq-Locations by RELAT_1:62; :: thesis: verum