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;

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

consider N1 being Element of NAT such that
A2: for n being Element of NAT st n >= N1 holds
g . n >= 0 by Def4;
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;
set a = max N,N1;
A7: max N,N1 >= N1 by XXREAL_0:25;
A8: max N,N1 >= N 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 A9: n >= a ; :: thesis: ( g . n <= (d " ) * (f . n) & g . n >= 0 )
then n >= N by A8, XXREAL_0:2;
then t . n >= d * (g . n) by A6;
then (d " ) * (t . n) >= (d " ) * (d * (g . n)) by A5, 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
n >= N1 by A7, A9, XXREAL_0:2;
hence g . n >= 0 by A2; :: thesis: verum

end;

hence g in Big_Oh f by A1, A5; :: 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
A10: g = t and
A11: 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
A12: c > 0 and
A13: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A11;
consider N1 being Element of NAT such that
A14: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
set a = max N,N1;
A15: max N,N1 >= N1 by XXREAL_0:25;
A16: max N,N1 >= N by XXREAL_0:25;

A17: 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 A18: n >= a ; :: thesis: ( f . n >= (c " ) * (g . n) & f . n >= 0 )
then n >= N by A16, XXREAL_0:2;
then t . n <= c * (f . n) by A13;
then (c " ) * (t . n) <= (c " ) * (c * (f . n)) by A12, XREAL_1:66;
then (c " ) * (t . n) <= ((c " ) * c) * (f . n) ;
then (c " ) * (t . n) <= 1 * (f . n) by A12, XCMPLX_0:def 7;
hence f . n >= (c " ) * (g . n) by A10; :: thesis: f . n >= 0
n >= N1 by A15, A18, XXREAL_0:2;
hence f . n >= 0 by A14; :: thesis: verum

end;

f is Element of Funcs NAT ,REAL by FUNCT_2:11;
hence f in Big_Omega g by A12, A17; :: thesis: verum