theorem :: DBLSEQ_2:10

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