theorem Th40: :: DBLSEQ_3:40

for f being Function of [:NAT,NAT:],ExtREAL holds
( ~ (Partial_Sums_in_cod1 f) = Partial_Sums_in_cod2 (~ f) & ~ (Partial_Sums_in_cod2 f) = Partial_Sums_in_cod1 (~ f) )