theorem Th8: :: DBLSEQ_3:8

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 )