let n be Element of NAT ; :: thesis: for x being real number st n > 0 & x = 1 / (n + 1) holds
(n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x)
let x be real number ; :: 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₁( Element of NAT ) -> set = x ^ ($1 + 1);
consider seq being Real_Sequence such that
A3: for k being Element of NAT holds seq . k = H₁(k) from SEQ_1:sch 1();

A4: now

let k be Element of 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:13
.= (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, Th39; :: thesis: verum

end;

A6: seq . 0 = x ^ (0 + 1) by A3
.= x by POWER:30 ;
A7: eseq ^\ (n + 1) is summable by Th24, SERIES_1:15;
n + 1 > 0 + 1 by A1, XREAL_1:8;
then A8: x < 1 by A2, XREAL_1:214;

A9: now

let k be Element of 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:32
.= x * (x ^ (k + 1)) by POWER:30
.= x * (seq . k) by A3 ; :: thesis: verum

end;

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