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