let c be non negative Real; :: thesis: for x, f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds
x in Big_Oh (c + f)
let x, f be eventually-nonnegative Real_Sequence; :: thesis: ( x in Big_Oh f implies x in Big_Oh (c + f) )
assume x in Big_Oh f ; :: thesis: x in Big_Oh (c + f)
then consider t being Element of Funcs (NAT,REAL) such that
A1: x = t and
A2: ex c1 being Real ex N being Element of NAT st
( c1 > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c1 * (f . n) & t . n >= 0 ) ) ) ;
consider c1 being Real, N being Element of NAT such that
A3: c1 > 0 and
A4: for n being Element of NAT st n >= N holds
( t . n <= c1 * (f . n) & t . n >= 0 ) by A2;
now :: thesis: for n being Element of NAT st n >= N holds
( t . n <= c1 * ((c + f) . n) & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= N implies ( t . n <= c1 * ((c + f) . n) & t . n >= 0 ) )
(f . n) + 0 <= (f . n) + c by XREAL_1:7;
then f . n <= (c + f) . n by VALUED_1:2;
then A5: c1 * (f . n) <= c1 * ((c + f) . n) by A3, XREAL_1:64;
assume A6: n >= N ; :: thesis: ( t . n <= c1 * ((c + f) . n) & t . n >= 0 )
then t . n <= c1 * (f . n) by A4;
hence ( t . n <= c1 * ((c + f) . n) & t . n >= 0 ) by A4, A6, A5, XXREAL_0:2; :: thesis: verum
end;
hence x in Big_Oh (c + f) by A1, A3; :: thesis: verum