for n being Element of NAT st n >= 1 holds
for f being Real_Sequence
for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds
f . n >= (n to_power (k + 1)) / (k + 1)