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

let x, y be Real_Sequence; :: thesis: ( x in Big_Oh () & y in Big_Oh () implies x + y in Big_Oh () )
assume AS: ( x in Big_Oh () & y in Big_Oh () ) ; :: thesis: x + y in Big_Oh ()
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 * (() . 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 * (() . 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 * (() . 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 * (() . 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) * (() . n) & (x + y) . n >= 0 )
proof
let n be Element of NAT ; :: thesis: ( n >= N1 + N2 implies ( (x + y) . n <= (c1 + c2) * (() . n) & (x + y) . n >= 0 ) )
assume X3: n >= N1 + N2 ; :: thesis: ( (x + y) . n <= (c1 + c2) * (() . n) & (x + y) . n >= 0 )
( N1 <= N1 + N2 & N2 <= N1 + N2 ) by NAT_1:11;
then X4: ( N1 <= n & N2 <= n ) by ;
then X5: ( x . n <= c1 * (() . n) & x . n >= 0 ) by P11;
X6: ( y . n <= c2 * (() . n) & y . n >= 0 ) by ;
(x . n) + (y . n) <= (c1 * (() . n)) + (c2 * (() . n)) by ;
hence ( (x + y) . n <= (c1 + c2) * (() . n) & (x + y) . n >= 0 ) by ; :: thesis: verum
end;
x + y is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence x + y in Big_Oh () by P11, P21, X2; :: thesis: verum