let n be Nat; :: thesis: for x being Real st n > 0 & x = 1 / (n + 1) holds
(n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x)
let x be Real; :: thesis: ( n > 0 & x = 1 / (n + 1) implies (n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x) )
assume that
A1: n > 0 and
A2: x = 1 / (n + 1) ; :: thesis: (n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x)
deffunc H₁( Nat) -> object = x ^ ($1 + 1);
consider seq being Real_Sequence such that
A3: for k being Nat holds seq . k = H₁(k) from SEQ_1:sch 1();

A4: now :: thesis: for k being Nat holds
( ((n !) (#) (eseq ^\ (n + 1))) . k >= 0 & ((n !) (#) (eseq ^\ (n + 1))) . k <= seq . k )

let k be Nat; :: thesis: ( ((n !) (#) (eseq ^\ (n + 1))) . k >= 0 & ((n !) (#) (eseq ^\ (n + 1))) . k <= seq . k )
A5: ((n !) (#) (eseq ^\ (n + 1))) . k = (n !) * ((eseq ^\ (n + 1)) . k) by SEQ_1:9
.= (n !) * (eseq . ((n + 1) + k)) by NAT_1:def 3
.= (n !) * (1 / (((n + k) + 1) !)) by Def5
.= (n !) / (((n + k) + 1) !) ;
hence ((n !) (#) (eseq ^\ (n + 1))) . k >= 0 ; :: thesis: ((n !) (#) (eseq ^\ (n + 1))) . k <= seq . k
seq . k = x ^ (k + 1) by A3;
hence ((n !) (#) (eseq ^\ (n + 1))) . k <= seq . k by A2, A5, Th38; :: thesis: verum

end;

A6: seq . 0 = x ^ (0 + 1) by A3
.= x ;
A7: eseq ^\ (n + 1) is summable by Th23, SERIES_1:12;
n + 1 > 0 + 1 by A1, XREAL_1:6;
then A8: x < 1 by A2, XREAL_1:212;

A9: now :: thesis: for k being Nat holds seq . (k + 1) = x * (seq . k)

let k be Nat; :: thesis: seq . (k + 1) = x * (seq . k)
thus seq . (k + 1) = x ^ ((k + 1) + 1) by A3
.= (x ^ 1) * (x ^ (k + 1)) by A2, POWER:27
.= x * (x ^ (k + 1))
.= x * (seq . k) by A3 ; :: thesis: verum

end;

|.x.| = x by A2, ABSVALUE:def 1;
then seq is summable by A8, A9, SERIES_1:25;
then A10: Sum ((n !) (#) (eseq ^\ (n + 1))) <= Sum seq by A4, SERIES_1:20;
|.x.| < 1 by A2, A8, ABSVALUE:def 1;
then Sum seq = x / (1 - x) by A6, A9, SERIES_1:25;
hence (n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x) by A7, A10, SERIES_1:10; :: thesis: verum