theorem Th46: :: DBLSEQ_3:46

for f1 being without-infty Function of [:NAT,NAT:],ExtREAL
for f2 being without+infty Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums_in_cod2 (f1 - f2) = (Partial_Sums_in_cod2 f1) - (Partial_Sums_in_cod2 f2) & Partial_Sums_in_cod1 (f1 - f2) = (Partial_Sums_in_cod1 f1) - (Partial_Sums_in_cod1 f2) & Partial_Sums_in_cod2 (f2 - f1) = (Partial_Sums_in_cod2 f2) - (Partial_Sums_in_cod2 f1) & Partial_Sums_in_cod1 (f2 - f1) = (Partial_Sums_in_cod1 f2) - (Partial_Sums_in_cod1 f1) )