let k be Nat; :: thesis: for c being XFinSequence of REAL st len c = k + 1 & seq_p c is eventually-nonnegative holds
seq_p c in Big_Oh ()

let c be XFinSequence of REAL ; :: thesis: ( len c = k + 1 & seq_p c is eventually-nonnegative implies seq_p c in Big_Oh () )
assume AS: ( len c = k + 1 & seq_p c is eventually-nonnegative ) ; :: thesis: seq_p c in Big_Oh ()
consider d being XFinSequence of REAL such that
P1: ( len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) ) by LMXFIN15;
T11: 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 = |.(c . i).| by P1;
hence 0 <= d . i by COMPLEX1:46; :: thesis: verum
end;
for r being Real st r in rng d holds
0 <= r
proof
let r be Real; :: thesis: ( r in rng d implies 0 <= r )
assume r in rng d ; :: thesis: 0 <= r
then consider x being object such that
RC: ( x in dom d & r = d . x ) by FUNCT_1:def 3;
thus 0 <= r by ; :: thesis: verum
end;
then d is nonnegative-yielding ;
then seq_p d in Big_Oh () by ;
then consider t being Element of Funcs (NAT,REAL) such that
P5: ( seq_p d = t & ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (() . n) & t . n >= 0 ) ) ) ) ;
consider N1 being Nat such that
P4A: for n being Nat st N1 <= n holds
0 <= () . n by AS;
consider a being Real, N2 being Element of NAT such that
P6: ( a > 0 & ( for n being Element of NAT st n >= N2 holds
( t . n <= a * (() . n) & t . n >= 0 ) ) ) by P5;
set N = N1 + N2;
P7: for n being Element of NAT st n >= N1 + N2 holds
( () . n <= a * (() . n) & () . n >= 0 )
proof
let n be Element of NAT ; :: thesis: ( n >= N1 + N2 implies ( () . n <= a * (() . n) & () . n >= 0 ) )
assume P8: n >= N1 + N2 ; :: thesis: ( () . n <= a * (() . n) & () . n >= 0 )
( N1 <= N1 + N2 & N2 <= N1 + N2 ) by NAT_1:11;
then P9: ( N1 <= n & N2 <= n ) by ;
then P10: ( (seq_p c) . n <= () . n & 0 <= () . n ) by ;
( (seq_p d) . n <= a * (() . n) & () . n >= 0 ) by P5, P9, P6;
hence (seq_p c) . n <= a * (() . n) by ; :: thesis: () . n >= 0
thus 0 <= () . n by ; :: thesis: verum
end;
seq_p c is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence seq_p c in Big_Oh () by P6, P7; :: thesis: verum