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