let f be FinSeq-Location ; :: thesis: not f in NAT
f in SCM+FSA-Data*-Loc by SCMFSA_2:def 5;
hence not f in NAT by SCMFSA_2:14, XBOOLE_0:3; :: thesis: verum