theorem Th7: :: DBLSEQ_3:7

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