let m be positive Nat; :: thesis: ( (m |^ (m + 1)) rExpSeq is convergent & lim ((m |^ (m + 1)) rExpSeq) = 0 )
(m |^ (m + 1)) rExpSeq is summable by SIN_COS:45;
hence ( (m |^ (m + 1)) rExpSeq is convergent & lim ((m |^ (m + 1)) rExpSeq) = 0 ) by SERIES_1:4; :: thesis: verum