theorem FNK: :: RVSUM_4:8

for n being Nat
for m being non zero Nat
for f being b₁ + b₂ -element FinSequence holds f | (n + 1) = (f | n) ^ <*(f . (n + 1))*>