theorem Th1: :: NDIFF_4:1

for m being Element of NAT
for f1, f2 being PartFunc of REAL,(REAL m) holds f1 - f2 = f1 + (- f2)