let k be Nat; :: thesis: for d being XFinSequence of REAL
for a being Real
for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds
ex N being Nat st
for x being Nat st N <= x holds
|.(() . x).| <= y . x

let d be XFinSequence of REAL ; :: thesis: for a being Real
for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds
ex N being Nat st
for x being Nat st N <= x holds
|.(() . x).| <= y . x

let a be Real; :: thesis: for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds
ex N being Nat st
for x being Nat st N <= x holds
|.(() . x).| <= y . x

let y be Real_Sequence; :: thesis: ( 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) implies ex N being Nat st
for x being Nat st N <= x holds
|.(() . x).| <= y . x )

assume that
A1: 0 < a and
A2: len d = k and
A3: for x being Nat holds y . x = a * (x to_power k) ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(() . x).| <= y . x

per cases ( k = 0 or k <> 0 ) ;
suppose K1: k = 0 ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(() . x).| <= y . x

set N = 0 ;
take 0 ; :: thesis: for x being Nat st 0 <= x holds
|.(() . x).| <= y . x

thus for x being Nat st 0 <= x holds
|.(() . x).| <= y . x :: thesis: verum
proof
let x be Nat; :: thesis: ( 0 <= x implies |.(() . x).| <= y . x )
assume 0 <= x ; :: thesis: |.(() . x).| <= y . x
D2: |.(() . x).| = 0 by ;
y . x = a * (x to_power k) by A3;
hence |.(() . x).| <= y . x by D2, A1; :: thesis: verum
end;
end;
suppose B4: k <> 0 ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(() . x).| <= y . x

rng |.d.| c= REAL ;
then reconsider c = |.d.| as XFinSequence of REAL by RELAT_1:def 19;
B3: for i being Nat st i in dom c holds
0 <= c . i
proof
let i be Nat; :: thesis: ( i in dom c implies 0 <= c . i )
assume i in dom c ; :: thesis: 0 <= c . i
then c . i = |.(d . i).| by VALUED_1:def 11;
hence 0 <= c . i by COMPLEX1:46; :: thesis: verum
end;
for r being Real st r in rng c holds
0 <= r
proof
let r be Real; :: thesis: ( r in rng c implies 0 <= r )
assume r in rng c ; :: thesis: 0 <= r
then consider x being object such that
RC: ( x in dom c & r = c . x ) by FUNCT_1:def 3;
thus 0 <= r by RC, B3; :: thesis: verum
end;
then B3T: c is nonnegative-yielding ;
len c = k by ;
then consider N being Nat such that
A4: for x being Nat st N <= x holds
for i being Nat st i in dom c holds
((c . i) * (x to_power i)) * k <= a * (x to_power k) by ;
take N ; :: thesis: for x being Nat st N <= x holds
|.(() . x).| <= y . x

thus for x being Nat st N <= x holds
|.(() . x).| <= y . x :: thesis: verum
proof
let x be Nat; :: thesis: ( N <= x implies |.(() . x).| <= y . x )
assume A0: N <= x ; :: thesis: |.(() . x).| <= y . x
NN0: dom (c (#) (seq_a^ (x,1,0))) = dom c by LMXFIN1
.= dom d by VALUED_1:def 11 ;
P1: (seq_p c) . x = Sum (c (#) (seq_a^ (x,1,0))) by defseqp;
for i being Nat st i in dom (c (#) (seq_a^ (x,1,0))) holds
(c (#) (seq_a^ (x,1,0))) . i <= (y . x) / k
proof
let i be Nat; :: thesis: ( i in dom (c (#) (seq_a^ (x,1,0))) implies (c (#) (seq_a^ (x,1,0))) . i <= (y . x) / k )
assume i in dom (c (#) (seq_a^ (x,1,0))) ; :: thesis: (c (#) (seq_a^ (x,1,0))) . i <= (y . x) / k
then X5: i in dom c by LMXFIN1;
then (((c . i) * (x to_power i)) * k) / k <= (a * (x to_power k)) / k by ;
then (c . i) * (x to_power i) <= (a * (x to_power k)) / k by ;
then (c . i) * (x to_power i) <= (y . x) / k by A3;
hence (c (#) (seq_a^ (x,1,0))) . i <= (y . x) / k by ; :: thesis: verum
end;
then Sum (c (#) (seq_a^ (x,1,0))) <= ((y . x) / k) * (len (c (#) (seq_a^ (x,1,0)))) by AFINSQ_2:59;
then P6: (seq_p c) . x <= y . x by ;
|.(() . x).| <= () . x by TLNEG41;
hence |.(() . x).| <= y . x by ; :: thesis: verum
end;
end;
end;