theorem FNK: :: RVSUM_4:8
for n being Nat
for m being non zero Nat
for f being b1 + b2 -element FinSequence holds f | (n + 1) = (f | n) ^ <*(f . (n + 1))*>