theorem Tr2: :: DBLSEQ_2:9

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