theorem Th110: :: NUMBER17:110

for s being Nat
for f being b₁ + 1 -element natural-valued non-decreasing positive FinSequence holds
( f . 1 <= (s + 1) / (Sum (f ")) & Sum ((Del (f,1)) ") = (Sum (f ")) - (1 / (f . 1)) )