theorem :: DBLSEQ_3:16

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