let l be FinSeq-Location ; :: thesis: Values l = INT *
l in SCM+FSA-Data*-Loc by Def5;
hence Values l = INT * by SCMFSA_1:11; :: thesis: verum