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