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 3;
A6: b <> 1 by ASYMPT_0:def 3;
A7: b > 0 by ASYMPT_0:def 3;
A8: a > 0 by ASYMPT_0:def 3;

now

let x be set ; :: 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

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:64 ;
N + 1 > N + 0 by XREAL_1:10;
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:65;
then log a,b > 0 by A8, A5, POWER:59;
then c * (log a,b) > c * 0 by A11, XREAL_1:70;
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

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:64 ;
N + 1 > N + 0 by XREAL_1:10;
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:65;
then log b,a > 0 by A7, A6, POWER:59;
then c * (log b,a) > c * 0 by A19, XREAL_1:70;
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