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 in Big_Theta (seq_n^ (k + 1))