let a be Real; :: thesis: ( 0 < a implies for k being Nat
for d being nonnegative-yielding XFinSequence of REAL st len d = k holds
ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) )

assume AS: 0 < a ; :: thesis: for k being Nat
for d being nonnegative-yielding XFinSequence of REAL st len d = k holds
ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

let k be Nat; :: thesis: for d being nonnegative-yielding XFinSequence of REAL st len d = k holds
ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

let d be nonnegative-yielding XFinSequence of REAL ; :: thesis: ( len d = k implies ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) )

assume A1: len d = k ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

A2: for i being Nat st i in dom d holds
0 <= d . i
proof
let i be Nat; :: thesis: ( i in dom d implies 0 <= d . i )
assume i in dom d ; :: thesis: 0 <= d . i
then d . i in rng d by FUNCT_1:3;
hence 0 <= d . i by PARTFUN3:def 4; :: thesis: verum
end;
per cases ( k = 0 or k <> 0 ) ;
suppose P0: k = 0 ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

set N = 0 ;
take 0 ; :: thesis: for x being Nat st 0 <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

let x be Nat; :: thesis: ( 0 <= x implies for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) )

assume 0 <= x ; :: thesis: for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

thus for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) by P0, A1; :: thesis: verum
end;
suppose K1P: k <> 0 ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

then 0 <= k - 1 by ;
then reconsider k1 = k - 1 as Nat by ;
consider M being Real such that
Q1: ( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) ) by ;
set N = [/((M * k) / a)\] + 2;
MM1: (M * k) / a <= [/((M * k) / a)\] by INT_1:def 7;
Q20P: 0 <= (M * k) / a by AS, Q1;
then Q20: 1 + 0 < 2 + [/((M * k) / a)\] by ;
[/((M * k) / a)\] + 2 in NAT by ;
then reconsider N = [/((M * k) / a)\] + 2 as Nat ;
([/((M * k) / a)\] + 1) + 0 < ([/((M * k) / a)\] + 1) + 1 by XREAL_1:8;
then (M * k) / a < N by ;
then ((M * k) / a) * a <= N * a by ;
then Q2: ( M * k <= a * N & 1 < N ) by ;
take N ; :: thesis: for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

thus for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) :: thesis: verum
proof
let x be Nat; :: thesis: ( N <= x implies for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k) )

assume Q3: N <= x ; :: thesis: for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)

let i be Nat; :: thesis: ( i in dom d implies ((d . i) * (x to_power i)) * k <= a * (x to_power k) )
assume Q4: i in dom d ; :: thesis: ((d . i) * (x to_power i)) * k <= a * (x to_power k)
then (d . i) * k <= M * k by ;
then Q5: ((d . i) * k) * (x to_power i) <= (M * k) * (x to_power i) by XREAL_1:64;
i in Segm k by Q4, A1;
then i < k1 + 1 by NAT_1:44;
then Y1: i <= k1 by NAT_1:13;
Y2: 1 < x by ;
X1: x to_power i <= x to_power k1 N1: x * (x to_power k1) = x to_power k
proof
per cases ( x = 0 or x <> 0 ) ;
suppose x = 0 ; :: thesis: x * (x to_power k1) = x to_power k
hence x * (x to_power k1) = x to_power k by ; :: thesis: verum
end;
suppose XX1: x <> 0 ; :: thesis: x * (x to_power k1) = x to_power k
x = x to_power 1 by POWER:25;
hence x * (x to_power k1) = x to_power (1 + k1) by
.= x to_power k ;
:: thesis: verum
end;
end;
end;
(M * k) * (x to_power i) <= (M * k) * (x to_power k1) by ;
then Q7: ((d . i) * k) * (x to_power i) <= (M * k) * (x to_power k1) by ;
(M * k) * (x to_power k1) <= (a * N) * (x to_power k1) by ;
then Q8: ((d . i) * k) * (x to_power i) <= (a * N) * (x to_power k1) by ;
a * N <= a * x by ;
then (a * N) * (x to_power k1) <= (a * x) * (x to_power k1) by XREAL_1:64;
hence ((d . i) * (x to_power i)) * k <= a * (x to_power k) by ; :: thesis: verum
end;
end;
end;