theorem Lm1: :: LTLAXIO5:1

for X being set
for f being FinSequence of X
for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i