theorem CNM: :: RVSUM_4:1

for f being Relation
for n, m being Nat holds (f | (n + m)) | n = f | n