let k be Nat; :: thesis: for x, y being Real_Sequence st x in Big_Oh (seq_n^ k) & y in Big_Oh (seq_n^ k) holds

x + y in Big_Oh (seq_n^ k)

let x, y be Real_Sequence; :: thesis: ( x in Big_Oh (seq_n^ k) & y in Big_Oh (seq_n^ k) implies x + y in Big_Oh (seq_n^ k) )

assume AS: ( x in Big_Oh (seq_n^ k) & y in Big_Oh (seq_n^ k) ) ; :: thesis: x + y in Big_Oh (seq_n^ k)

consider t being Element of Funcs (NAT,REAL) such that

P1: ( x = 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 * ((seq_n^ k) . n) & t . n >= 0 ) ) ) ) by AS;

consider w being Element of Funcs (NAT,REAL) such that

P2: ( y = w & ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( w . n <= c * ((seq_n^ k) . n) & w . n >= 0 ) ) ) ) by AS;

consider c1 being Real, N1 being Element of NAT such that

P11: ( c1 > 0 & ( for n being Element of NAT st n >= N1 holds

( x . n <= c1 * ((seq_n^ k) . n) & x . n >= 0 ) ) ) by P1;

consider c2 being Real, N2 being Element of NAT such that

P21: ( c2 > 0 & ( for n being Element of NAT st n >= N2 holds

( y . n <= c2 * ((seq_n^ k) . n) & y . n >= 0 ) ) ) by P2;

set c = c1 + c2;

set N = N1 + N2;

X2: for n being Element of NAT st n >= N1 + N2 holds

( (x + y) . n <= (c1 + c2) * ((seq_n^ k) . n) & (x + y) . n >= 0 )

hence x + y in Big_Oh (seq_n^ k) by P11, P21, X2; :: thesis: verum

x + y in Big_Oh (seq_n^ k)

let x, y be Real_Sequence; :: thesis: ( x in Big_Oh (seq_n^ k) & y in Big_Oh (seq_n^ k) implies x + y in Big_Oh (seq_n^ k) )

assume AS: ( x in Big_Oh (seq_n^ k) & y in Big_Oh (seq_n^ k) ) ; :: thesis: x + y in Big_Oh (seq_n^ k)

consider t being Element of Funcs (NAT,REAL) such that

P1: ( x = 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 * ((seq_n^ k) . n) & t . n >= 0 ) ) ) ) by AS;

consider w being Element of Funcs (NAT,REAL) such that

P2: ( y = w & ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( w . n <= c * ((seq_n^ k) . n) & w . n >= 0 ) ) ) ) by AS;

consider c1 being Real, N1 being Element of NAT such that

P11: ( c1 > 0 & ( for n being Element of NAT st n >= N1 holds

( x . n <= c1 * ((seq_n^ k) . n) & x . n >= 0 ) ) ) by P1;

consider c2 being Real, N2 being Element of NAT such that

P21: ( c2 > 0 & ( for n being Element of NAT st n >= N2 holds

( y . n <= c2 * ((seq_n^ k) . n) & y . n >= 0 ) ) ) by P2;

set c = c1 + c2;

set N = N1 + N2;

X2: for n being Element of NAT st n >= N1 + N2 holds

( (x + y) . n <= (c1 + c2) * ((seq_n^ k) . n) & (x + y) . n >= 0 )

proof

x + y is Element of Funcs (NAT,REAL)
by FUNCT_2:8;
let n be Element of NAT ; :: thesis: ( n >= N1 + N2 implies ( (x + y) . n <= (c1 + c2) * ((seq_n^ k) . n) & (x + y) . n >= 0 ) )

assume X3: n >= N1 + N2 ; :: thesis: ( (x + y) . n <= (c1 + c2) * ((seq_n^ k) . n) & (x + y) . n >= 0 )

( N1 <= N1 + N2 & N2 <= N1 + N2 ) by NAT_1:11;

then X4: ( N1 <= n & N2 <= n ) by X3, XXREAL_0:2;

then X5: ( x . n <= c1 * ((seq_n^ k) . n) & x . n >= 0 ) by P11;

X6: ( y . n <= c2 * ((seq_n^ k) . n) & y . n >= 0 ) by P21, X4;

(x . n) + (y . n) <= (c1 * ((seq_n^ k) . n)) + (c2 * ((seq_n^ k) . n)) by X5, X6, XREAL_1:7;

hence ( (x + y) . n <= (c1 + c2) * ((seq_n^ k) . n) & (x + y) . n >= 0 ) by SEQ_1:7, X5, X6; :: thesis: verum

end;assume X3: n >= N1 + N2 ; :: thesis: ( (x + y) . n <= (c1 + c2) * ((seq_n^ k) . n) & (x + y) . n >= 0 )

( N1 <= N1 + N2 & N2 <= N1 + N2 ) by NAT_1:11;

then X4: ( N1 <= n & N2 <= n ) by X3, XXREAL_0:2;

then X5: ( x . n <= c1 * ((seq_n^ k) . n) & x . n >= 0 ) by P11;

X6: ( y . n <= c2 * ((seq_n^ k) . n) & y . n >= 0 ) by P21, X4;

(x . n) + (y . n) <= (c1 * ((seq_n^ k) . n)) + (c2 * ((seq_n^ k) . n)) by X5, X6, XREAL_1:7;

hence ( (x + y) . n <= (c1 + c2) * ((seq_n^ k) . n) & (x + y) . n >= 0 ) by SEQ_1:7, X5, X6; :: thesis: verum

hence x + y in Big_Oh (seq_n^ k) by P11, P21, X2; :: thesis: verum