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 Element of NAT such that
A2: for n being Element of NAT st n >= N2 holds
g . n >= 0 by Def4;
consider N1 being Element of NAT such that
A3: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
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

let x be set ; :: 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;
set a = max N,(max N1,N2);
A10: max N,(max N1,N2) >= N by XXREAL_0:25;
A11: max N,(max N1,N2) >= max N1,N2 by XXREAL_0:25;
max N1,N2 >= N2 by XXREAL_0:25;
then A12: max N,(max N1,N2) >= N2 by A11, XXREAL_0:2;
max N1,N2 >= N1 by XXREAL_0:25;
then A13: max N,(max N1,N2) >= N1 by A11, XXREAL_0:2;

A14: now

let n be Element of NAT ; :: thesis: ( n >= max N,(max N1,N2) 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 Def10;
( (f + g) . n = (f . n) + (g . n) & f . n <= max (f . n),(g . n) ) by SEQ_1:11, XXREAL_0:25;
then (f + g) . n <= 2 * ((max f,g) . n) by A16, A15, XREAL_1:9;
then A17: c * ((f + g) . n) <= c * (2 * ((max f,g) . n)) by A7, XREAL_1:66;
assume A18: n >= max N,(max N1,N2) ; :: 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:9;
hence (max f,g) . n <= (f + g) . n by SEQ_1:11; :: 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:9;
hence (max f,g) . n <= (f + g) . n by SEQ_1:11; :: thesis: verum

end;

end;

end;

then A21: d * ((max f,g) . n) <= d * ((f + g) . n) by A8, XREAL_1:66;
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:70;
hence x in Big_Theta (max f,g) by A1, A5, A8, A14; :: thesis: verum

end;

consider N1 being Element of NAT such that
A22: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
consider N2 being Element of NAT such that
A23: for n being Element of NAT st n >= N2 holds
g . n >= 0 by Def4;
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;
set a = max N,(max N1,N2);
A29: max N1,N2 <= max N,(max N1,N2) by XXREAL_0:25;
N2 <= max N1,N2 by XXREAL_0:25;
then A30: N2 <= max N,(max N1,N2) by A29, XXREAL_0:2;
A31: N <= max N,(max N1,N2) by XXREAL_0:25;
N1 <= max N1,N2 by XXREAL_0:25;
then A32: N1 <= max N,(max N1,N2) by A29, XXREAL_0:2;

A33: now

let n be Element of NAT ; :: thesis: ( n >= max N,(max N1,N2) implies ( (d * (2 " )) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) )
assume A34: n >= max N,(max N1,N2) ; :: 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:9;
( 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:9;
then (2 " ) * ((f . n) + (g . n)) <= (2 " ) * (2 * (max (f . n),(g . n))) by XREAL_1:66;
then (2 " ) * ((f + g) . n) <= max (f . n),(g . n) by SEQ_1:11;
then d * ((2 " ) * ((f + g) . n)) <= d * (max (f . n),(g . n)) by A27, XREAL_1:66;
then A36: d * ((2 " ) * ((f + g) . n)) <= d * ((max f,g) . n) by Def10;
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:9;
( (max f,g) . n = max (f . n),(g . n) & (f + g) . n = (f . n) + (g . n) ) by Def10, SEQ_1:11;
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:66;
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:70;
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