:: deftheorem Def3 defines FinSeq-Location SCMFSA_2:def 5 :
for b₁ being Object of SCM+FSA holds
( b₁ is FinSeq-Location iff b₁ in SCM+FSA-Data*-Loc );