for rseq1, rseq2 being convergent Real_Sequence holds
( addreal * (rseq1,rseq2) is convergent_in_cod1 & addreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (addreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )