- (k + 1) < - 0 by XREAL_1:24;
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 Def3; :: thesis: verum