let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: Partial_Sums (Rseq1 + Rseq2) = (Partial_Sums Rseq1) + (Partial_Sums Rseq2)
Partial_Sums (Rseq1 + Rseq2) = Partial_Sums_in_cod2 ((Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2)) by thADD;
hence Partial_Sums (Rseq1 + Rseq2) = (Partial_Sums Rseq1) + (Partial_Sums Rseq2) by thADD; :: thesis: verum