theorem Th24: :: LIOUVIL1:25

for f being eventually-non-zero Real_Sequence
for n being Nat holds f ^\ n is eventually-non-zero