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

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

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

now :: thesis:

reconsider N = N as Nat ;
take N = N; :: thesis:
let n be Nat; :: thesis:
A6: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis:
hence t . n >= 0 by A5, A6; :: thesis:

end;

then A7: t is eventually-nonnegative ;
t in Big_Omega f by A4;
hence x in Big_Omega g by A3, A7, A2, Th21; :: thesis:

end;

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

now :: thesis:

reconsider N = N as Nat ;
take N = N; :: thesis:
let n be Nat; :: thesis:
A11: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis:
hence t . n >= 0 by A10, A11; :: thesis:

end;

then A12: t is eventually-nonnegative ;
f in Big_Oh f by Th10;
then f in Big_Oh g by A1, Th15;
then A13: g in Big_Omega f by Th19;
t in Big_Omega g by A9;
hence x in Big_Omega f by A8, A12, A13, Th21; :: thesis:

end;

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