theorem Th8: :: MESFUNC2:8
for C being non empty set
for f1, f2 being PartFunc of C,ExtREAL holds f1 - f2 = f1 + (- f2)