set q = seq_const 1;
set p = seq_n^ 1;
set f = (seq_n^ 1) - (seq_const 1);
set g = seq_n^ 1;
A1: Big_Theta (seq_n^ 1) = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((seq_n^ 1) . n) <= t . n & t . n <= c * ((seq_n^ 1) . n) ) ) ) } by ASYMPT_0:27;
let F be eventually-nonnegative Real_Sequence; :: thesis: ( F = (seq_n^ 1) - (seq_const 1) implies (Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1) )
assume F = (seq_n^ 1) - (seq_const 1) ; :: thesis: (Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1)
then A2: Big_Theta F = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (((seq_n^ 1) - (seq_const 1)) . n) <= t . n & t . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) ) ) ) } by ASYMPT_0:27;

now :: thesis: for x being object holds
( ( x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) implies x in Big_Theta (seq_n^ 1) ) & ( x in Big_Theta (seq_n^ 1) implies x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) ) )

let x be object ; :: thesis: ( ( x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) implies x in Big_Theta (seq_n^ 1) ) & ( x in Big_Theta (seq_n^ 1) implies x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) ) )

hereby :: thesis: ( x in Big_Theta (seq_n^ 1) implies x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) )

assume x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) ; :: thesis: x in Big_Theta (seq_n^ 1)
then consider t being Element of Funcs (NAT,REAL) such that
A3: t = x and
A4: ex f9, g9 being Element of Funcs (NAT,REAL) st
( f9 in Big_Theta F & g9 in Big_Theta (seq_n^ 1) & ( for n being Element of NAT holds t . n = (f9 . n) + (g9 . n) ) ) ;
consider f9, g9 being Element of Funcs (NAT,REAL) such that
A5: f9 in Big_Theta F and
A6: g9 in Big_Theta (seq_n^ 1) and
A7: for n being Element of NAT holds t . n = (f9 . n) + (g9 . n) by A4;
ex r being Element of Funcs (NAT,REAL) st
( r = f9 & ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (((seq_n^ 1) - (seq_const 1)) . n) <= r . n & r . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) ) ) ) ) by A2, A5;
then consider c1, d1 being Real, N1 being Element of NAT such that
A8: c1 > 0 and
A9: d1 > 0 and
A10: for n being Element of NAT st n >= N1 holds
( d1 * (((seq_n^ 1) - (seq_const 1)) . n) <= f9 . n & f9 . n <= c1 * (((seq_n^ 1) - (seq_const 1)) . n) ) ;
ex s being Element of Funcs (NAT,REAL) st
( s = g9 & ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((seq_n^ 1) . n) <= s . n & s . n <= c * ((seq_n^ 1) . n) ) ) ) ) by A1, A6;
then consider c2, d2 being Real, N2 being Element of NAT such that
A11: c2 > 0 and
A12: d2 > 0 and
A13: for n being Element of NAT st n >= N2 holds
( d2 * ((seq_n^ 1) . n) <= g9 . n & g9 . n <= c2 * ((seq_n^ 1) . n) ) ;
set d = d2;
set c = c1 + c2;
set N = max (1,(max (N1,N2)));
A14: max (1,(max (N1,N2))) >= 1 by XXREAL_0:25;
A15: max (1,(max (N1,N2))) >= max (N1,N2) by XXREAL_0:25;
max (N1,N2) >= N2 by XXREAL_0:25;
then A16: max (1,(max (N1,N2))) >= N2 by A15, XXREAL_0:2;
max (N1,N2) >= N1 by XXREAL_0:25;
then A17: max (1,(max (N1,N2))) >= N1 by A15, XXREAL_0:2;

now :: thesis: for n being Element of NAT st n >= max (1,(max (N1,N2))) holds
( d2 * ((seq_n^ 1) . n) <= t . n & t . n <= (c1 + c2) * ((seq_n^ 1) . n) )

let n be Element of NAT ; :: thesis: ( n >= max (1,(max (N1,N2))) implies ( d2 * ((seq_n^ 1) . n) <= t . n & t . n <= (c1 + c2) * ((seq_n^ 1) . n) ) )
A18: (seq_const 1) . n = 1 by FUNCOP_1:7;
assume A19: n >= max (1,(max (N1,N2))) ; :: thesis: ( d2 * ((seq_n^ 1) . n) <= t . n & t . n <= (c1 + c2) * ((seq_n^ 1) . n) )
then A20: (seq_n^ 1) . n = n to_power 1 by A14, Def3
.= n by POWER:25 ;
n >= 1 by A14, A19, XXREAL_0:2;
then - n <= - 1 by XREAL_1:24;
then (- n) * d1 <= (- 1) * d1 by A9, XREAL_1:64;
then A21: (n * (- d1)) + ((d1 + d2) * n) <= (- d1) + ((d1 + d2) * n) by XREAL_1:6;
A22: ((seq_n^ 1) - (seq_const 1)) . n = ((seq_n^ 1) . n) + ((- (seq_const 1)) . n) by SEQ_1:7
.= ((seq_n^ 1) . n) + (- ((seq_const 1) . n)) by SEQ_1:10
.= (n to_power 1) + (- ((seq_const 1) . n)) by A14, A19, Def3
.= n + (- 1) by A18, POWER:25 ;
A23: n >= N2 by A16, A19, XXREAL_0:2;
then d2 * ((seq_n^ 1) . n) <= g9 . n by A13;
then A24: (d1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (d2 * ((seq_n^ 1) . n)) <= (d1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (g9 . n) by XREAL_1:6;
g9 . n <= c2 * ((seq_n^ 1) . n) by A13, A23;
then A25: (c1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (g9 . n) <= (c1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (c2 * ((seq_n^ 1) . n)) by XREAL_1:6;
A26: n >= N1 by A17, A19, XXREAL_0:2;
then f9 . n <= c1 * (((seq_n^ 1) - (seq_const 1)) . n) by A10;
then (f9 . n) + (g9 . n) <= (c1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (g9 . n) by XREAL_1:6;
then A27: (f9 . n) + (g9 . n) <= (c1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (c2 * ((seq_n^ 1) . n)) by A25, XXREAL_0:2;
d1 * (((seq_n^ 1) - (seq_const 1)) . n) <= f9 . n by A10, A26;
then (d1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (g9 . n) <= (f9 . n) + (g9 . n) by XREAL_1:6;
then (d1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (d2 * ((seq_n^ 1) . n)) <= (f9 . n) + (g9 . n) by A24, XXREAL_0:2;
then d2 * n <= (f9 . n) + (g9 . n) by A20, A22, A21, XXREAL_0:2;
hence d2 * ((seq_n^ 1) . n) <= t . n by A7, A20; :: thesis: t . n <= (c1 + c2) * ((seq_n^ 1) . n)
(- c1) + ((c1 + c2) * n) <= 0 + ((c1 + c2) * n) by A8, XREAL_1:6;
then (f9 . n) + (g9 . n) <= (c1 + c2) * n by A20, A22, A27, XXREAL_0:2;
hence t . n <= (c1 + c2) * ((seq_n^ 1) . n) by A7, A20; :: thesis: verum

end;

hence x in Big_Theta (seq_n^ 1) by A1, A3, A8, A11, A12; :: thesis: verum

end;

assume x in Big_Theta (seq_n^ 1) ; :: thesis: x in (Big_Theta F) + (Big_Theta (seq_n^ 1))
then consider t being Element of Funcs (NAT,REAL) such that
A28: t = x and
A29: ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((seq_n^ 1) . n) <= t . n & t . n <= c * ((seq_n^ 1) . n) ) ) ) by A1;
consider c, d being Real, N being Element of NAT such that
A30: c > 0 and
A31: d > 0 and
A32: for n being Element of NAT st n >= N holds
( d * ((seq_n^ 1) . n) <= t . n & t . n <= c * ((seq_n^ 1) . n) ) by A29;
set f9 = (2 ") (#) t;
set g9 = (2 ") (#) t;
A33: (2 ") (#) t is Element of Funcs (NAT,REAL) by FUNCT_2:8;
A34: for n being Element of NAT holds t . n = (((2 ") (#) t) . n) + (((2 ") (#) t) . n)

proof

let n be Element of NAT ; :: thesis: t . n = (((2 ") (#) t) . n) + (((2 ") (#) t) . n)
((2 ") (#) t) . n = (2 ") * (t . n) by SEQ_1:9;
hence t . n = (((2 ") (#) t) . n) + (((2 ") (#) t) . n) ; :: thesis: verum

end;

A35: (2 ") * d > (2 ") * 0 by A31, XREAL_1:68;
set N0 = max (N,2);
A36: max (N,2) >= N by XXREAL_0:25;
A37: max (N,2) >= 2 by XXREAL_0:25;
reconsider N0 = max (N,2) as Element of NAT ;

A38: now :: thesis: for n being Element of NAT st n >= N0 holds
( ((2 ") * d) * ((seq_n^ 1) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= ((2 ") * c) * ((seq_n^ 1) . n) )

let n be Element of NAT ; :: thesis: ( n >= N0 implies ( ((2 ") * d) * ((seq_n^ 1) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= ((2 ") * c) * ((seq_n^ 1) . n) ) )
assume n >= N0 ; :: thesis: ( ((2 ") * d) * ((seq_n^ 1) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= ((2 ") * c) * ((seq_n^ 1) . n) )
then A39: n >= N by A36, XXREAL_0:2;
then A40: (2 ") * (t . n) <= (2 ") * (c * ((seq_n^ 1) . n)) by A32, XREAL_1:64;
(2 ") * (d * ((seq_n^ 1) . n)) <= (2 ") * (t . n) by A32, A39, XREAL_1:64;
hence ( ((2 ") * d) * ((seq_n^ 1) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= ((2 ") * c) * ((seq_n^ 1) . n) ) by A40, SEQ_1:9; :: thesis: verum

end;

(2 ") * c > (2 ") * 0 by A30, XREAL_1:68;
then A41: (2 ") (#) t in Big_Theta (seq_n^ 1) by A1, A35, A33, A38;

now :: thesis: for n being Element of NAT st n >= N0 holds
( ((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) )

let n be Element of NAT ; :: thesis: ( n >= N0 implies ( ((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) ) )
A42: (seq_const 1) . n = 1 by FUNCOP_1:7;
assume A43: n >= N0 ; :: thesis: ( ((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) )
then A44: (seq_n^ 1) . n = (n to_power 1) - 0 by A37, Def3
.= n - 0 by POWER:25 ;
n >= 2 by A37, A43, XXREAL_0:2;
then n + 2 <= n + n by XREAL_1:6;
then n <= (2 * n) - (2 * 1) by XREAL_1:19;
then (2 ") * n <= (2 ") * (2 * (n - 1)) by XREAL_1:64;
then A45: c * ((2 ") * n) <= c * (n - 1) by A30, XREAL_1:64;
A46: n >= N by A36, A43, XXREAL_0:2;
then A47: (2 ") * (d * ((seq_n^ 1) . n)) <= (2 ") * (t . n) by A32, XREAL_1:64;
A48: ((seq_n^ 1) - (seq_const 1)) . n = ((seq_n^ 1) . n) + ((- (seq_const 1)) . n) by SEQ_1:7
.= ((seq_n^ 1) . n) + (- 1) by A42, SEQ_1:10
.= ((seq_n^ 1) . n) - 1
.= (n to_power 1) - 1 by A37, A43, Def3
.= n - 1 by POWER:25 ;
then ((seq_n^ 1) - (seq_const 1)) . n <= (seq_n^ 1) . n by A44, XREAL_1:13;
then ((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") * d) * ((seq_n^ 1) . n) by A31, XREAL_1:64;
then ((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= (2 ") * (t . n) by A47, XXREAL_0:2;
hence ((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") (#) t) . n by SEQ_1:9; :: thesis: ((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n)
(2 ") * (t . n) <= (2 ") * (c * ((seq_n^ 1) . n)) by A32, A46, XREAL_1:64;
then (2 ") * (t . n) <= c * (((seq_n^ 1) - (seq_const 1)) . n) by A48, A44, A45, XXREAL_0:2;
hence ((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) by SEQ_1:9; :: thesis: verum

end;

then (2 ") (#) t in Big_Theta F by A2, A30, A35, A33;
hence x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) by A28, A33, A41, A34; :: thesis: verum

end;

hence (Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1) by TARSKI:2; :: thesis: verum