theorem :: DBLSEQ_3:52

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