A1: ( seq_const 2 is convergent & lim (seq_const 2) = 2 ) ;
A2: geo-seq (2,1) is convergent by Th85;
A3: lim (geo-seq (2,1)) = 0 by Th85;
A4: lim (- (geo-seq (2,1))) = - (lim (geo-seq (2,1))) by SEQ_2:10, Th85
.= 0 by A3 ;
lim SumsReciTriang = 2 + 0 by SEQ_2:6, A1, A2, Th86, A4;
hence ( SumsReciTriang is convergent & lim SumsReciTriang = 2 ) by Th86, A2; :: thesis: verum