let s be State of SCM+FSA; :: thesis: FinSeq-Locations c= dom s
dom s = the carrier of SCM+FSA by PARTFUN1:def 2;
hence FinSeq-Locations c= dom s ; :: thesis: verum