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 lim (g /" f) = (lim (f /" g)) " by Th2;
then A2: g in Big_Oh f by A1, Lm3, Th2;
f in Big_Oh g by A1, Lm3;
hence Big_Oh f = Big_Oh g by A2, Lm2; :: thesis: verum