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 A1: ( n > 0 & x = 1 / (n + 1) ) ; :: thesis: (n ! ) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x)
then A2: n + 1 > 0 + 1 by XREAL_1:8;
A4: ( 0 < x & x < 1 ) by A1, A2, XREAL_1:214;
deffunc H₁( Element of NAT ) -> set = x ^ ($1 + 1);
consider seq being Real_Sequence such that
A5: for k being Element of NAT holds seq . k = H₁(k) from SEQ_1:sch 1();
A6: seq . 0 = x ^ (0 + 1) by A5
.= x by POWER:30 ;
A7: abs x = x by A1, ABSVALUE:def 1;
A8: abs x < 1 by A4, ABSVALUE:def 1;

A9: now

let k be Element of NAT ; :: thesis: seq . (k + 1) = x * (seq . k)
thus seq . (k + 1) = x ^ ((k + 1) + 1) by A5
.= (x ^ 1) * (x ^ (k + 1)) by A1, POWER:32
.= x * (x ^ (k + 1)) by POWER:30
.= x * (seq . k) by A5 ; :: thesis: verum

end;

then A10: ( seq is summable & Sum seq = (seq . 0 ) / (1 - x) ) by A4, A7, SERIES_1:29;
A11: Sum seq = x / (1 - x) by A6, A8, A9, SERIES_1:29;
A12: eseq ^\ (n + 1) is summable by Th24, SERIES_1:15;

now

let k be Element of NAT ; :: thesis: ( ((n ! ) (#) (eseq ^\ (n + 1))) . k >= 0 & ((n ! ) (#) (eseq ^\ (n + 1))) . k <= seq . k )
A13: ((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 A5;
hence ((n ! ) (#) (eseq ^\ (n + 1))) . k <= seq . k by A1, A13, Th39; :: thesis: verum

end;

then Sum ((n ! ) (#) (eseq ^\ (n + 1))) <= Sum seq by A10, SERIES_1:24;
hence (n ! ) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x) by A11, A12, SERIES_1:13; :: thesis: verum