theorem :: NUMBER12:22
for f being non-empty natural-valued increasing Arithmetic_Progression ex i, fi being Nat st
( fi = f . i & not fi is perfect_power )