:: deftheorem defines + INTEGR15:def 9 :
for n being Nat
for Z being set
for f, g being PartFunc of Z,(REAL n) holds f + g = f <++> g;