for n being Element of NAT
for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2