let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) > 0 implies f in Big_Theta g )
assume ( f /" g is convergent & lim (f /" g) > 0 ) ; :: thesis: f in Big_Theta g
then A1: Big_Oh f = Big_Oh g by Th15;
then A2: f in Big_Oh g by Th10;
g in Big_Oh f by A1, Th10;
then f in Big_Omega g by Th19;
hence f in Big_Theta g by A2, XBOOLE_0:def 4; :: thesis: verum