let f, g be eventually-nonnegative Real_Sequence; :: thesis: Big_Omega (f + g) = Big_Omega (max f,g)
consider N1 being Element of NAT such that
A1: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
consider N2 being Element of NAT such that
A2: for n being Element of NAT st n >= N2 holds
g . n >= 0 by Def4;

now

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

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

assume x in Big_Omega (f + g) ; :: thesis: x in Big_Omega (max f,g)
then consider t being Element of Funcs NAT ,REAL such that
A3: t = x and
A4: ex d being Real ex N being Element of NAT st
( d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((f + g) . n) <= t . n & t . n >= 0 ) ) ) ;
consider d being Real, N being Element of NAT such that
A5: d > 0 and
A6: for n being Element of NAT st n >= N holds
( d * ((f + g) . n) <= t . n & t . n >= 0 ) by A4;
set a = max N,(max N1,N2);
A7: max N,(max N1,N2) >= N by XXREAL_0:25;
A8: max N,(max N1,N2) >= max N1,N2 by XXREAL_0:25;
max N1,N2 >= N2 by XXREAL_0:25;
then A9: max N,(max N1,N2) >= N2 by A8, XXREAL_0:2;
max N1,N2 >= N1 by XXREAL_0:25;
then A10: max N,(max N1,N2) >= N1 by A8, XXREAL_0:2;

now

let n be Element of NAT ; :: thesis: ( n >= max N,(max N1,N2) implies ( d * ((max f,g) . n) <= t . n & t . n >= 0 ) )
assume A11: n >= max N,(max N1,N2) ; :: thesis: ( d * ((max f,g) . n) <= t . n & t . n >= 0 )
then n >= N1 by A10, XXREAL_0:2;
then A12: f . n >= 0 by A1;
n >= N2 by A9, A11, XXREAL_0:2;
then A13: g . n >= 0 by A2;
A14: (max f,g) . n = max (f . n),(g . n) by Def10;
(max f,g) . n <= (f + g) . n

proof

per cases ( (max f,g) . n = f . n or (max f,g) . n = g . n ) by A14, 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 A13, 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 A12, XREAL_1:9;
hence (max f,g) . n <= (f + g) . n by SEQ_1:11; :: thesis: verum

end;

end;

end;

then A15: d * ((max f,g) . n) <= d * ((f + g) . n) by A5, XREAL_1:66;
A16: n >= N by A7, A11, XXREAL_0:2;
then d * ((f + g) . n) <= t . n by A6;
hence d * ((max f,g) . n) <= t . n by A15, XXREAL_0:2; :: thesis: t . n >= 0
thus t . n >= 0 by A6, A16; :: thesis: verum

end;

hence x in Big_Omega (max f,g) by A3, A5; :: thesis: verum

end;

assume x in Big_Omega (max f,g) ; :: thesis: x in Big_Omega (f + g)
then consider t being Element of Funcs NAT ,REAL such that
A17: t = x and
A18: ex d being Real ex N being Element of NAT st
( d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((max f,g) . n) <= t . n & t . n >= 0 ) ) ) ;
consider d being Real, N being Element of NAT such that
A19: d > 0 and
A20: for n being Element of NAT st n >= N holds
( d * ((max f,g) . n) <= t . n & t . n >= 0 ) by A18;
set a = max N,(max N1,N2);
A21: N <= max N,(max N1,N2) by XXREAL_0:25;

A22: now

let n be Element of NAT ; :: thesis: ( n >= max N,(max N1,N2) implies ( (d * (2 " )) * ((f + g) . n) <= t . n & t . n >= 0 ) )
( 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 A19, XREAL_1:66;
then A23: d * ((2 " ) * ((f + g) . n)) <= d * ((max f,g) . n) by Def10;
assume n >= max N,(max N1,N2) ; :: thesis: ( (d * (2 " )) * ((f + g) . n) <= t . n & t . n >= 0 )
then A24: n >= N by A21, XXREAL_0:2;
then d * ((max f,g) . n) <= t . n by A20;
hence (d * (2 " )) * ((f + g) . n) <= t . n by A23, XXREAL_0:2; :: thesis: t . n >= 0
thus t . n >= 0 by A20, A24; :: thesis: verum

end;

d * (2 " ) > d * 0 by A19, XREAL_1:70;
hence x in Big_Omega (f + g) by A17, A22; :: thesis: verum

end;

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