let f, g be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Omega g iff g in Big_Oh f )
A1: g is Element of Funcs NAT ,REAL by FUNCT_2:11;
A2: f is Element of Funcs NAT ,REAL by FUNCT_2:11;

hereby :: thesis: ( g in Big_Oh f implies f in Big_Omega g )

assume f in Big_Omega g ; :: thesis: g in Big_Oh f
then consider t being Element of Funcs NAT ,REAL such that
A3: f = t 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
( t . n >= d * (g . 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
( t . n >= d * (g . n) & t . n >= 0 ) by A4;
A7: d " > 0 by A5;
consider N1 being Element of NAT such that
A8: for n being Element of NAT st n >= N1 holds
g . n >= 0 by Def4;
set a = max N,N1;
A9: ( max N,N1 >= N & max N,N1 >= N1 ) by XXREAL_0:25;

now

take a = max N,N1; :: thesis: for n being Element of NAT st n >= a holds
( g . n <= (d " ) * (f . n) & g . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a implies ( g . n <= (d " ) * (f . n) & g . n >= 0 ) )
assume n >= a ; :: thesis: ( g . n <= (d " ) * (f . n) & g . n >= 0 )
then A10: ( n >= N & n >= N1 ) by A9, XXREAL_0:2;
then ( t . n >= d * (g . n) & t . n >= 0 ) by A6;
then (d " ) * (t . n) >= (d " ) * (d * (g . n)) by A7, XREAL_1:66;
then (d " ) * (t . n) >= ((d " ) * d) * (g . n) ;
then (d " ) * (t . n) >= 1 * (g . n) by A5, XCMPLX_0:def 7;
hence g . n <= (d " ) * (f . n) by A3; :: thesis: g . n >= 0
thus g . n >= 0 by A8, A10; :: thesis: verum

end;

hence g in Big_Oh f by A1, A7; :: thesis: verum

end;

assume g in Big_Oh f ; :: thesis: f in Big_Omega g
then consider t being Element of Funcs NAT ,REAL such that
A11: g = t and
A12: 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 * (f . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A13: c > 0 and
A14: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A12;
A15: c " > 0 by A13;
consider N1 being Element of NAT such that
A16: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
set a = max N,N1;
A17: ( max N,N1 >= N & max N,N1 >= N1 ) by XXREAL_0:25;

now

take a = max N,N1; :: thesis: for n being Element of NAT st n >= a holds
( f . n >= (c " ) * (g . n) & f . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a implies ( f . n >= (c " ) * (g . n) & f . n >= 0 ) )
assume n >= a ; :: thesis: ( f . n >= (c " ) * (g . n) & f . n >= 0 )
then A18: ( n >= N & n >= N1 ) by A17, XXREAL_0:2;
then ( t . n <= c * (f . n) & t . n >= 0 ) by A14;
then (c " ) * (t . n) <= (c " ) * (c * (f . n)) by A15, XREAL_1:66;
then (c " ) * (t . n) <= ((c " ) * c) * (f . n) ;
then (c " ) * (t . n) <= 1 * (f . n) by A13, XCMPLX_0:def 7;
hence f . n >= (c " ) * (g . n) by A11; :: thesis: f . n >= 0
thus f . n >= 0 by A16, A18; :: thesis: verum

end;

hence f in Big_Omega g by A2, A15; :: thesis: verum
thus verum ; :: thesis: verum