theorem Th21: :: IRRAT_1:21
for n being Nat st n > 0 holds
( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n )