for fl being FinSeq-Location ex i being Nat st fl = fsloc i