theorem Th44: :: E_TRANS2:38

for m being positive Nat holds
( (m |^ (m + 1)) rExpSeq is convergent & lim ((m |^ (m + 1)) rExpSeq) = 0 )