theorem :: DBLSEQ_3:13

for f1 being without-infty Function of [:NAT,NAT:],ExtREAL
for f2 being without+infty Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds
( (f1 - f2) . (n,m) = (f1 . (n,m)) - (f2 . (n,m)) & (f2 - f1) . (n,m) = (f2 . (n,m)) - (f1 . (n,m)) )