theorem Th4: :: REAL_NS3:4

for n being Nat
for x, y being Element of REAL n
for m being Nat st m <= n holds
(x - y) | m = (x | m) - (y | m)