theorem Th110: :: FINSEQ_3:112

for k, n being Nat
for f being FinSequence st k <= n holds
(f | n) . k = f . k