let a, b be logbase Real; :: thesis: 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 )
let f, g be Real_Sequence; :: thesis: ( 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) ) implies ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = g & Big_Oh s = Big_Oh s1 ) )
assume that
A1: a > 1 and
A2: b > 1 and
A3: for n being Element of NAT st n > 0 holds
f . n = log (a,n) and
A4: for n being Element of NAT st n > 0 holds
g . n = log (b,n) ; :: thesis: ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = g & Big_Oh s = Big_Oh s1 )
reconsider g = g as eventually-positive Real_Sequence by A2, A4, Lm2;
reconsider f = f as eventually-positive Real_Sequence by A1, A3, Lm2;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = f & s1 = g & Big_Oh f = Big_Oh s1 )
take g ; :: thesis: ( f = f & g = g & Big_Oh f = Big_Oh g )
A5: a <> 1 by ASYMPT_0:def 1;
A6: b <> 1 by ASYMPT_0:def 1;
A7: b > 0 by ASYMPT_0:def 1;
A8: a > 0 by ASYMPT_0:def 1;

now :: thesis: for x being object holds
( ( x in Big_Oh f implies x in Big_Oh g ) & ( x in Big_Oh g implies x in Big_Oh f ) )

let x be object ; :: thesis: ( ( x in Big_Oh f implies x in Big_Oh g ) & ( x in Big_Oh g implies x in Big_Oh f ) )

hereby :: thesis: ( x in Big_Oh g implies x in Big_Oh f )

assume x in Big_Oh f ; :: thesis: x in Big_Oh g
then consider t being Element of Funcs (NAT,REAL) such that
A9: x = t and
A10: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A11: c > 0 and
A12: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A10;

A13: now :: thesis: ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
( t . n <= (c * (log (a,b))) * (g . n) & t . n >= 0 )

take N1 = N + 1; :: thesis: for n being Element of NAT st n >= N1 holds
( t . n <= (c * (log (a,b))) * (g . n) & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= N1 implies ( t . n <= (c * (log (a,b))) * (g . n) & t . n >= 0 ) )
assume A14: n >= N1 ; :: thesis: ( t . n <= (c * (log (a,b))) * (g . n) & t . n >= 0 )
then A15: f . n = log (a,n) by A3
.= (log (a,b)) * (log (b,n)) by A8, A5, A7, A6, A14, POWER:56 ;
N + 1 > N + 0 by XREAL_1:8;
then A16: n > N by A14, XXREAL_0:2;
then t . n <= c * (f . n) by A12;
then t . n <= (c * (log (a,b))) * (log (b,n)) by A15;
hence t . n <= (c * (log (a,b))) * (g . n) by A4, A14; :: thesis: t . n >= 0
thus t . n >= 0 by A12, A16; :: thesis: verum

end;

log (a,b) > log (a,1) by A1, A2, POWER:57;
then log (a,b) > 0 by A8, A5, POWER:51;
then c * (log (a,b)) > c * 0 by A11, XREAL_1:68;
hence x in Big_Oh g by A9, A13; :: thesis: verum

end;

assume x in Big_Oh g ; :: thesis: x in Big_Oh f
then consider t being Element of Funcs (NAT,REAL) such that
A17: x = t and
A18: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (g . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A19: c > 0 and
A20: for n being Element of NAT st n >= N holds
( t . n <= c * (g . n) & t . n >= 0 ) by A18;

A21: now :: thesis: ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
( t . n <= (c * (log (b,a))) * (f . n) & t . n >= 0 )

take N1 = N + 1; :: thesis: for n being Element of NAT st n >= N1 holds
( t . n <= (c * (log (b,a))) * (f . n) & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= N1 implies ( t . n <= (c * (log (b,a))) * (f . n) & t . n >= 0 ) )
assume A22: n >= N1 ; :: thesis: ( t . n <= (c * (log (b,a))) * (f . n) & t . n >= 0 )
then A23: g . n = log (b,n) by A4
.= (log (b,a)) * (log (a,n)) by A8, A5, A7, A6, A22, POWER:56 ;
N + 1 > N + 0 by XREAL_1:8;
then A24: n > N by A22, XXREAL_0:2;
then t . n <= c * (g . n) by A20;
then t . n <= (c * (log (b,a))) * (log (a,n)) by A23;
hence t . n <= (c * (log (b,a))) * (f . n) by A3, A22; :: thesis: t . n >= 0
thus t . n >= 0 by A20, A24; :: thesis: verum

end;

log (b,a) > log (b,1) by A1, A2, POWER:57;
then log (b,a) > 0 by A7, A6, POWER:51;
then c * (log (b,a)) > c * 0 by A19, XREAL_1:68;
hence x in Big_Oh f by A17, A21; :: thesis: verum

end;

hence ( f = f & g = g & Big_Oh f = Big_Oh g ) by TARSKI:2; :: thesis: verum