theorem CNX: :: RVSUM_4:2

for f being Function
for n being Nat
for m being non zero Nat holds (f | (n + m)) . n = f . n