theorem :: INTEGR15:22

for n being Nat
for Z, x being set
for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds
(f - g) /. x = (f /. x) - (g /. x)