let a be Real; :: thesis: for k being Nat ex c being non empty positive-yielding XFinSequence of REAL st
for x being Nat holds a * (x to_power k) <= (polynom c) . x
let k be Nat; :: thesis: ex c being non empty positive-yielding XFinSequence of REAL st
for x being Nat holds a * (x to_power k) <= (polynom c) . x
reconsider c = (Segm (k + 1)) --> (|.a.| + 1) as XFinSequence of REAL ;
reconsider c = c as non empty positive-yielding XFinSequence of REAL ;
take c ; :: thesis: for x being Nat holds a * (x to_power k) <= (polynom c) . x
for x being Nat holds a * (x to_power k) <= (polynom c) . x

proof

let x be Nat; :: thesis: a * (x to_power k) <= (polynom c) . x
set c2 = c (#) (seq_a^ (x,1,0));
T0: (polynom c) . x = Sum (c (#) (seq_a^ (x,1,0))) by ASYMPT_2:def 2;
LN2: k + 0 < k + 1 by XREAL_1:8;
T1: dom (c (#) (seq_a^ (x,1,0))) = (dom c) /\ (dom (seq_a^ (x,1,0))) by VALUED_1:def 4
.= (dom c) /\ NAT by SEQ_1:1
.= (Segm (k + 1)) /\ NAT ;
T3: (c (#) (seq_a^ (x,1,0))) . k = (c . k) * ((seq_a^ (x,1,0)) . k) by VALUED_1:5
.= (c . k) * (x to_power ((1 * k) + 0)) by ASYMPT_1:def 1
.= (|.a.| + 1) * (x to_power k) by FUNCOP_1:7, NAT_1:44, LN2 ;
a < |.a.| + 1 by TCL001;
then T4: a * (x to_power k) <= (|.a.| + 1) * (x to_power k) by XREAL_1:64;
len (c (#) (seq_a^ (x,1,0))) = k + 1 by T1, XBOOLE_1:28;
then Sum (c (#) (seq_a^ (x,1,0))) >= (|.a.| + 1) * (x to_power k) by T3, AFINSQ_2:61, NAT_1:44, LN2;
hence a * (x to_power k) <= (polynom c) . x by T4, XXREAL_0:2, T0; :: thesis: verum

end;

hence for x being Nat holds a * (x to_power k) <= (polynom c) . x ; :: thesis: verum