theorem Th9: :: DBLSEQ_3:9

for X being non empty set
for f1, f2 being without+infty Function of X,ExtREAL holds
( f1 + f2 = f1 - (- f2) & - (f1 + f2) = (- f1) - f2 )