reconsider k = k as Element of NAT by ORDINAL1:def 13;
- (k + 1) < - 0 by XREAL_1:26;
then ( - (k + 1) in INT & not - (k + 1) in NAT ) by INT_1:def 1;
then - (k + 1) in SCM+FSA-Data*-Loc by XBOOLE_0:def 5;
hence - (k + 1) is FinSeq-Location by Def5; :: thesis: verum