for i being Nat
for f being one-to-one FinSequence st i in dom f holds
(f . i) .. f = i