let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) > 0 implies Big_Oh f = Big_Oh g )
assume A1: ( f /" g is convergent & lim (f /" g) > 0 ) ; :: thesis: Big_Oh f = Big_Oh g
then A2: f in Big_Oh g by Lm3;
A3: ( g /" f is convergent & lim (g /" f) = (lim (f /" g)) " ) by A1, Th2;
(lim (f /" g)) " > 0 by A1;
then g in Big_Oh f by A3, Lm3;
hence Big_Oh f = Big_Oh g by A2, Lm2; :: thesis: verum