theorem Th39: :: DBLSEQ_3:39

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