let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) > 0 implies Big_Omega f = Big_Omega g )
assume A1: ( f /" g is convergent & lim (f /" g) > 0 ) ; :: thesis: Big_Omega f = Big_Omega g

now

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

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

assume x in Big_Omega f ; :: thesis: x in Big_Omega g
then consider t being Element of Funcs NAT ,REAL such that
A2: x = t and
A3: 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 . n) <= t . n & t . n >= 0 ) ) ) ;
consider d being Real, N being Element of NAT such that
d > 0 and
A4: for n being Element of NAT st n >= N holds
( d * (f . n) <= t . n & t . n >= 0 ) by A3;

now

take N = N; :: thesis: for n being Element of NAT st n >= N holds
t . n >= 0
let n be Element of NAT ; :: thesis: ( n >= N implies t . n >= 0 )
assume n >= N ; :: thesis: t . n >= 0
hence t . n >= 0 by A4; :: thesis: verum

end;

then A5: t is eventually-nonnegative by Def4;
A6: t in Big_Omega f by A3;
g in Big_Oh g by Th10;
then g in Big_Oh f by A1, Th15;
then f in Big_Omega g by Th19;
hence x in Big_Omega g by A2, A5, A6, Th21; :: thesis: verum

end;

assume x in Big_Omega g ; :: thesis: x in Big_Omega f
then consider t being Element of Funcs NAT ,REAL such that
A7: x = t and
A8: ex d being Real ex N being Element of NAT st
( d > 0 & ( for n being Element of NAT st n >= N holds
( d * (g . n) <= t . n & t . n >= 0 ) ) ) ;
consider d being Real, N being Element of NAT such that
d > 0 and
A9: for n being Element of NAT st n >= N holds
( d * (g . n) <= t . n & t . n >= 0 ) by A8;

now

take N = N; :: thesis: for n being Element of NAT st n >= N holds
t . n >= 0
let n be Element of NAT ; :: thesis: ( n >= N implies t . n >= 0 )
assume n >= N ; :: thesis: t . n >= 0
hence t . n >= 0 by A9; :: thesis: verum

end;

then A10: t is eventually-nonnegative by Def4;
A11: t in Big_Omega g by A8;
f in Big_Oh f by Th10;
then f in Big_Oh g by A1, Th15;
then g in Big_Omega f by Th19;
hence x in Big_Omega f by A7, A10, A11, Th21; :: thesis: verum

end;

hence Big_Omega f = Big_Omega g by TARSKI:2; :: thesis: verum