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