let fl be FinSeq-Location ; :: thesis: ex i being Nat st fl = fsloc i
A1: fl in SCM+FSA-Data*-Loc by Def3;
then consider k being Nat such that
A2: ( fl = k or fl = - k ) by INT_1:def 1;
k <> 0 by A1, A2, XBOOLE_0:def 5;
then consider i being Nat such that
A3: k = i + 1 by NAT_1:6;
reconsider i = i as Nat ;
take i ; :: thesis: fl = fsloc i
thus fl = fsloc i by A1, A2, A3, XBOOLE_0:def 5; :: thesis: verum