let d be XFinSequence of REAL ; :: thesis: for k being Nat st len d = 1 & d is nonnegative-yielding holds

seq_p d in Big_Oh (seq_n^ k)

let k be Nat; :: thesis: ( len d = 1 & d is nonnegative-yielding implies seq_p d in Big_Oh (seq_n^ k) )

assume AS: ( len d = 1 & d is nonnegative-yielding ) ; :: thesis: seq_p d in Big_Oh (seq_n^ k)

then consider a being Real such that

P1: ( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) ) by LMXFIN5;

set y = seq_p d;

set c = a + 1;

XA1: a + 0 < a + 1 by XREAL_1:8;

0 in Segm 1 by NAT_1:44;

then ASX: 0 <= d . 0 by AS, FUNCT_1:3;

hence seq_p d in Big_Oh (seq_n^ k) by A1, P1, ASX; :: thesis: verum

seq_p d in Big_Oh (seq_n^ k)

let k be Nat; :: thesis: ( len d = 1 & d is nonnegative-yielding implies seq_p d in Big_Oh (seq_n^ k) )

assume AS: ( len d = 1 & d is nonnegative-yielding ) ; :: thesis: seq_p d in Big_Oh (seq_n^ k)

then consider a being Real such that

P1: ( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) ) by LMXFIN5;

set y = seq_p d;

set c = a + 1;

XA1: a + 0 < a + 1 by XREAL_1:8;

0 in Segm 1 by NAT_1:44;

then ASX: 0 <= d . 0 by AS, FUNCT_1:3;

A1: now :: thesis: for n being Element of NAT st n >= 2 holds

( (seq_p d) . n <= (a + 1) * ((seq_n^ k) . n) & (seq_p d) . n >= 0 )

seq_p d is Element of Funcs (NAT,REAL)
by FUNCT_2:8;( (seq_p d) . n <= (a + 1) * ((seq_n^ k) . n) & (seq_p d) . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= 2 implies ( (seq_p d) . n <= (a + 1) * ((seq_n^ k) . n) & (seq_p d) . n >= 0 ) )

assume A2: n >= 2 ; :: thesis: ( (seq_p d) . n <= (a + 1) * ((seq_n^ k) . n) & (seq_p d) . n >= 0 )

then A3: n > 1 by XXREAL_0:2;

A4: (seq_n^ k) . n = n to_power k by A2, ASYMPT_1:def 3;

1 <= (seq_n^ k) . n then 1 * a <= ((seq_n^ k) . n) * (a + 1) by XA1, XREAL_1:66, P1, ASX;

hence (seq_p d) . n <= (a + 1) * ((seq_n^ k) . n) by P1; :: thesis: (seq_p d) . n >= 0

thus (seq_p d) . n >= 0 by P1, ASX; :: thesis: verum

end;assume A2: n >= 2 ; :: thesis: ( (seq_p d) . n <= (a + 1) * ((seq_n^ k) . n) & (seq_p d) . n >= 0 )

then A3: n > 1 by XXREAL_0:2;

A4: (seq_n^ k) . n = n to_power k by A2, ASYMPT_1:def 3;

1 <= (seq_n^ k) . n then 1 * a <= ((seq_n^ k) . n) * (a + 1) by XA1, XREAL_1:66, P1, ASX;

hence (seq_p d) . n <= (a + 1) * ((seq_n^ k) . n) by P1; :: thesis: (seq_p d) . n >= 0

thus (seq_p d) . n >= 0 by P1, ASX; :: thesis: verum

hence seq_p d in Big_Oh (seq_n^ k) by A1, P1, ASX; :: thesis: verum