let f, g be eventually-nonnegative Real_Sequence; :: thesis: Big_Theta (f + g) = Big_Theta (max (f,g))
A1: Big_Theta (max (f,g)) = { s where s 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 * ((max (f,g)) . n) <= s . n & s . n <= c * ((max (f,g)) . n) ) ) ) } by Th27;
consider N2 being Nat such that
A2: for n being Nat st n >= N2 holds
g . n >= 0 by Def2;
consider N1 being Nat such that
A3: for n being Nat st n >= N1 holds
f . n >= 0 by Def2;
A4: Big_Theta (f + g) = { s where s 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 * ((f + g) . n) <= s . n & s . n <= c * ((f + g) . n) ) ) ) } by Th27;

now :: thesis: for x being object holds
( ( x in Big_Theta (f + g) implies x in Big_Theta (max (f,g)) ) & ( x in Big_Theta (max (f,g)) implies x in Big_Theta (f + g) ) )

let x be object ; :: thesis: ( ( x in Big_Theta (f + g) implies x in Big_Theta (max (f,g)) ) & ( x in Big_Theta (max (f,g)) implies x in Big_Theta (f + g) ) )

hereby :: thesis: ( x in Big_Theta (max (f,g)) implies x in Big_Theta (f + g) )

assume x in Big_Theta (f + g) ; :: thesis: x in Big_Theta (max (f,g))
then consider t being Element of Funcs (NAT,REAL) such that
A5: t = x and
A6: 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 * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) ) ) by A4;
consider c, d being Real, N being Element of NAT such that
A7: c > 0 and
A8: d > 0 and
A9: for n being Element of NAT st n >= N holds
( d * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) by A6;
reconsider a = max (N,(max (N1,N2))) as Element of NAT by ORDINAL1:def 12;
A10: a >= N by XXREAL_0:25;
A11: a >= max (N1,N2) by XXREAL_0:25;
max (N1,N2) >= N2 by XXREAL_0:25;
then A12: a >= N2 by A11, XXREAL_0:2;
max (N1,N2) >= N1 by XXREAL_0:25;
then A13: a >= N1 by A11, XXREAL_0:2;

A14: now :: thesis: for n being Element of NAT st n >= a holds
( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) )

let n be Element of NAT ; :: thesis: ( n >= a implies ( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) ) )
A15: ( g . n <= max ((f . n),(g . n)) & (1 * ((max (f,g)) . n)) + (1 * ((max (f,g)) . n)) = (1 + 1) * ((max (f,g)) . n) ) by XXREAL_0:25;
A16: (max (f,g)) . n = max ((f . n),(g . n)) by Def7;
( (f + g) . n = (f . n) + (g . n) & f . n <= max ((f . n),(g . n)) ) by SEQ_1:7, XXREAL_0:25;
then (f + g) . n <= 2 * ((max (f,g)) . n) by A16, A15, XREAL_1:7;
then A17: c * ((f + g) . n) <= c * (2 * ((max (f,g)) . n)) by A7, XREAL_1:64;
assume A18: n >= a ; :: thesis: ( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) )
then n >= N2 by A12, XXREAL_0:2;
then A19: g . n >= 0 by A2;
n >= N1 by A13, A18, XXREAL_0:2;
then A20: f . n >= 0 by A3;
(max (f,g)) . n <= (f + g) . n

proof

per cases ( (max (f,g)) . n = f . n or (max (f,g)) . n = g . n ) by A16, XXREAL_0:16;

suppose (max (f,g)) . n = f . n ; :: thesis: (max (f,g)) . n <= (f + g) . n

then ((max (f,g)) . n) + 0 <= (f . n) + (g . n) by A19, XREAL_1:7;
hence (max (f,g)) . n <= (f + g) . n by SEQ_1:7; :: thesis: verum

end;

suppose (max (f,g)) . n = g . n ; :: thesis: (max (f,g)) . n <= (f + g) . n

then ((max (f,g)) . n) + 0 <= (g . n) + (f . n) by A20, XREAL_1:7;
hence (max (f,g)) . n <= (f + g) . n by SEQ_1:7; :: thesis: verum

end;

end;

end;

then A21: d * ((max (f,g)) . n) <= d * ((f + g) . n) by A8, XREAL_1:64;
n >= N by A10, A18, XXREAL_0:2;
then ( t . n <= c * ((f + g) . n) & d * ((f + g) . n) <= t . n ) by A9;
hence ( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) ) by A17, A21, XXREAL_0:2; :: thesis: verum

end;

2 * c > 2 * 0 by A7, XREAL_1:68;
hence x in Big_Theta (max (f,g)) by A1, A5, A8, A14; :: thesis: verum

end;

consider N1 being Nat such that
A22: for n being Nat st n >= N1 holds
f . n >= 0 by Def2;
consider N2 being Nat such that
A23: for n being Nat st n >= N2 holds
g . n >= 0 by Def2;
assume x in Big_Theta (max (f,g)) ; :: thesis: x in Big_Theta (f + g)
then consider t being Element of Funcs (NAT,REAL) such that
A24: t = x and
A25: 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 * ((max (f,g)) . n) <= t . n & t . n <= c * ((max (f,g)) . n) ) ) ) by A1;
consider c, d being Real, N being Element of NAT such that
A26: c > 0 and
A27: d > 0 and
A28: for n being Element of NAT st n >= N holds
( d * ((max (f,g)) . n) <= t . n & t . n <= c * ((max (f,g)) . n) ) by A25;
reconsider a = max (N,(max (N1,N2))) as Element of NAT by ORDINAL1:def 12;
A29: max (N1,N2) <= a by XXREAL_0:25;
N2 <= max (N1,N2) by XXREAL_0:25;
then A30: N2 <= a by A29, XXREAL_0:2;
A31: N <= a by XXREAL_0:25;
N1 <= max (N1,N2) by XXREAL_0:25;
then A32: N1 <= a by A29, XXREAL_0:2;

A33: now :: thesis: for n being Element of NAT st n >= a holds
( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) )

let n be Element of NAT ; :: thesis: ( n >= a implies ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) )
assume A34: n >= a ; :: thesis: ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) )
then n >= N1 by A32, XXREAL_0:2;
then f . n >= 0 by A22;
then A35: (f . n) + (g . n) >= 0 + (g . n) by XREAL_1:7;
( f . n <= max ((f . n),(g . n)) & g . n <= max ((f . n),(g . n)) ) by XXREAL_0:25;
then (f . n) + (g . n) <= (1 * (max ((f . n),(g . n)))) + (1 * (max ((f . n),(g . n)))) by XREAL_1:7;
then (2 ") * ((f . n) + (g . n)) <= (2 ") * (2 * (max ((f . n),(g . n)))) by XREAL_1:64;
then (2 ") * ((f + g) . n) <= max ((f . n),(g . n)) by SEQ_1:7;
then d * ((2 ") * ((f + g) . n)) <= d * (max ((f . n),(g . n))) by A27, XREAL_1:64;
then A36: d * ((2 ") * ((f + g) . n)) <= d * ((max (f,g)) . n) by Def7;
n >= N2 by A30, A34, XXREAL_0:2;
then g . n >= 0 by A23;
then A37: (f . n) + (g . n) >= (f . n) + 0 by XREAL_1:7;
( (max (f,g)) . n = max ((f . n),(g . n)) & (f + g) . n = (f . n) + (g . n) ) by Def7, SEQ_1:7;
then (max (f,g)) . n <= (f + g) . n by A37, A35, XXREAL_0:16;
then A38: c * ((max (f,g)) . n) <= c * ((f + g) . n) by A26, XREAL_1:64;
n >= N by A31, A34, XXREAL_0:2;
then ( t . n <= c * ((max (f,g)) . n) & d * ((max (f,g)) . n) <= t . n ) by A28;
hence ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) by A38, A36, XXREAL_0:2; :: thesis: verum

end;

d * (2 ") > d * 0 by A27, XREAL_1:68;
hence x in Big_Theta (f + g) by A4, A24, A26, A33; :: thesis: verum

end;

hence Big_Theta (f + g) = Big_Theta (max (f,g)) by TARSKI:2; :: thesis: verum