theorem Th4: :: SCMFSA_2:9

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