let c be non empty positive-yielding XFinSequence of REAL ; :: thesis: ex a being Real ex k, N being Nat st
( 0 < a & 0 < k & ( for x being Nat st N <= x holds
(polynom c) . x <= a * (x to_power k) ) )
1 - 1 <= (len c) - 1 by XREAL_1:9, NAT_1:14;
then (len c) - 1 in NAT by INT_1:3;
then reconsider k = (len c) - 1 as Nat ;
C1: len c = k + 1 ;
(k + 1) - 1 < (len c) - 0 by XREAL_1:15;
then k in Segm (len c) by NAT_1:44;
then C2: c . k in rng c by FUNCT_1:3;
for n being Nat st 0 <= n holds
0 <= (seq_p c) . n by NLM3;
then reconsider f = seq_p c as eventually-nonnegative Real_Sequence by ASYMPT_0:def 2;
f in Big_Oh (seq_n^ k) by ASYMPT_2:45, C1, C2, PARTFUN3:def 1;
then consider N being Nat such that
C5: for x being Nat st N <= x holds
f . x <= (seq_n^ (k + 1)) . x by ASYMPT_2:39;
reconsider m = k + 1 as Nat ;
reconsider M = N + 1 as Nat ;
take 1 ; :: thesis: ex k, N being Nat st
( 0 < 1 & 0 < k & ( for x being Nat st N <= x holds
(polynom c) . x <= 1 * (x to_power k) ) )
take m ; :: thesis: ex N being Nat st
( 0 < 1 & 0 < m & ( for x being Nat st N <= x holds
(polynom c) . x <= 1 * (x to_power m) ) )
take M ; :: thesis: ( 0 < 1 & 0 < m & ( for x being Nat st M <= x holds
(polynom c) . x <= 1 * (x to_power m) ) )
for x being Nat st M <= x holds
f . x <= 1 * (x to_power m)

proof

let x be Nat; :: thesis: ( M <= x implies f . x <= 1 * (x to_power m) )
assume C8: M <= x ; :: thesis: f . x <= 1 * (x to_power m)
CX: x is Element of NAT by ORDINAL1:def 12;
(N + 1) - 1 < M - 0 by XREAL_1:15;
then N < x by C8, XXREAL_0:2;
then f . x <= (seq_n^ m) . x by C5;
hence f . x <= 1 * (x to_power m) by C8, ASYMPT_1:def 3, CX; :: thesis: verum

end;

hence ( 0 < 1 & 0 < m & ( for x being Nat st M <= x holds
(polynom c) . x <= 1 * (x to_power m) ) ) ; :: thesis: verum