theorem Th11: :: DBLSEQ_3:11

for f1, 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))