for a, b being logbase Real
for f, g being Real_Sequence st a > 1 & b > 1 & ( for n being Element of NAT st n > 0 holds
f . n = log (a,n) ) & ( for n being Element of NAT st n > 0 holds
g . n = log (b,n) ) holds
ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = g & Big_Oh s = Big_Oh s1 )