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