set f = the FinSeq-Location ;
A1: the FinSeq-Location in SCM+FSA-Data*-Loc by SCMFSA_2:def 5;
assume not SCM+FSA-Data*-Loc <> NAT ; :: thesis: contradiction
hence contradiction by A1, Th4; :: thesis: verum