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 )

proof

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;

x + y is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence x + y in Big_Oh (seq_n^ k) by P11, P21, X2; :: thesis: verum