theorem :: DBLSEQ_3:52

for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being V184() 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) )