theorem Th26: :: FLEXARY1:26

for n being Nat
for f being natural-valued increasing FinSequence st n > 1 holds
((n |^ f) . 1) + (((n |^ f),2) +...) < 2 * (n |^ (f . (len f)))