theorem :: INTEGR15:21

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)