let s be Nat; :: thesis: for f being s + 1 -element natural-valued non-decreasing positive FinSequence holds
( f . 1 <= (s + 1) / (Sum (f ")) & Sum ((Del (f,1)) ") = (Sum (f ")) - (1 / (f . 1)) )
let f be s + 1 -element natural-valued non-decreasing positive FinSequence; :: thesis: ( f . 1 <= (s + 1) / (Sum (f ")) & Sum ((Del (f,1)) ") = (Sum (f ")) - (1 / (f . 1)) )
set u = Sum (f ");
set g = Del (f,1);
A1: len f = s + 1 by CARD_1:def 7;
defpred S₁[ FinSequence of NAT ] means for F being natural-valued non-decreasing positive FinSequence st F = $1 holds
Sum ($1 ") <= (len $1) / ($1 . 1);
A2: S₁[ <*> NAT] ;
A3: for p being FinSequence of NAT
for x being Element of NAT st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of NAT ; :: thesis: for x being Element of NAT st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of NAT ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A4: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
let P be natural-valued non-decreasing positive FinSequence; :: thesis: ( P = p ^ <*x*> implies Sum ((p ^ <*x*>) ") <= (len (p ^ <*x*>)) / ((p ^ <*x*>) . 1) )
assume A5: P = p ^ <*x*> ; :: thesis: Sum ((p ^ <*x*>) ") <= (len (p ^ <*x*>)) / ((p ^ <*x*>) . 1)
p is len p -element ;
then A6: P . 1 = p . 1 & ... & P . (len p) = p . (len p) by A5, FINSEQ_3:154;
A7: <*x*> " = <*(x ")*> by NUMBER15:63;

per cases ( len p < 1 or 1 <= len p ) ;

suppose len p < 1 ; :: thesis: Sum ((p ^ <*x*>) ") <= (len (p ^ <*x*>)) / ((p ^ <*x*>) . 1)

then p = {} by NAT_1:14;
then A8: P = <*x*> by A5, FINSEQ_1:34;
len <*x*> = 1 by FINSEQ_1:39;
hence Sum ((p ^ <*x*>) ") <= (len (p ^ <*x*>)) / ((p ^ <*x*>) . 1) by A5, A8, A7; :: thesis: verum

end;

suppose 1 <= len p ; :: thesis: Sum ((p ^ <*x*>) ") <= (len (p ^ <*x*>)) / ((p ^ <*x*>) . 1)

then A9: P . 1 = p . 1 by A6;
A10: len P = (len p) + 1 by A5, FINSEQ_2:16;
A11: P " = (p ") ^ (<*x*> ") by A5, NUMBER15:60;
A12: Sum (P ") = (Sum (p ")) + (x ") by A7, A11, RVSUM_1:74;
A13: p is non-decreasing by A5, Th37;
p is positive by A5, NUMBER08:37;
then A14: (Sum (p ")) + (x ") <= ((len p) / (p . 1)) + (x ") by A4, A13, XREAL_1:6;
A15: 1 <= 1 + (len p) by NAT_1:11;
then A16: 1 in dom P by A10, FINSEQ_3:25;
A17: len P in dom P by A10, A15, FINSEQ_3:25;
1 <= len P by A5, A10, XREAL_1:6;
then P . 1 <= P . (len P) by A16, A17, VALUED_0:def 15;
then (P . 1) " >= (P . (len P)) " by A5, XREAL_1:85;
then ((len p) / (p . 1)) + (x ") <= ((len p) / (p . 1)) + (1 / (p . 1)) by A9, A5, A10, XREAL_1:6;
hence Sum ((p ^ <*x*>) ") <= (len (p ^ <*x*>)) / ((p ^ <*x*>) . 1) by A9, A10, A12, A5, A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A18: for p being FinSequence of NAT holds S₁[p] from FINSEQ_2:sch 2(A2, A3);
reconsider F = f as FinSequence of NAT by FINSEQ_1:103;
S₁[F] by A18;
then (Sum (f ")) * (f . 1) <= ((s + 1) / (f . 1)) * (f . 1) by A1, XREAL_1:64;
then (Sum (f ")) * (f . 1) <= s + 1 by XCMPLX_1:87;
then ((Sum (f ")) * (f . 1)) / (Sum (f ")) <= (s + 1) / (Sum (f ")) by XREAL_1:64;
hence f . 1 <= (s + 1) / (Sum (f ")) by XCMPLX_1:89; :: thesis: Sum ((Del (f,1)) ") = (Sum (f ")) - (1 / (f . 1))
f = <*(f . 1)*> ^ (Del (f,1)) by FINSEQ_5:86;
then f " = (<*(f . 1)*> ") ^ ((Del (f,1)) ") by NUMBER15:60
.= <*((f . 1) ")*> ^ ((Del (f,1)) ") by NUMBER15:63 ;
then Sum (f ") = ((f . 1) ") + (Sum ((Del (f,1)) ")) by RVSUM_2:33;
hence Sum ((Del (f,1)) ") = (Sum (f ")) - (1 / (f . 1)) ; :: thesis: verum