let a, b be logbase Real; :: thesis: for f, g being Real_Sequence st a > 1 & b > 1 & f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log a,n ) & g . 0 = 0 & ( 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 & f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log a,n ) & g . 0 = 0 & ( 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: ( f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log a,n ) ) and
A4: ( g . 0 = 0 & ( 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 f = f as eventually-positive Real_Sequence by A1, A3, Lm2;
reconsider g = g as eventually-positive Real_Sequence by A2, A4, 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 > 0 & a <> 1 ) by ASYMPT_0:def 3;
A6: ( b > 0 & b <> 1 ) 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
A7: x = t and
A8: 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
A9: c > 0 and
A10: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A8;
log a,b > log a,1 by A1, A2, POWER:65;
then log a,b > 0 by A5, POWER:59;
then A11: c * (log a,b) > c * 0 by A9, XREAL_1:70;

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 A12: n >= N1 ; :: thesis: ( t . n <= (c * (log a,b)) * (g . n) & t . n >= 0 )
N + 1 > N + 0 by XREAL_1:10;
then A13: n > N by A12, XXREAL_0:2;
then A14: t . n <= c * (f . n) by A10;
f . n = log a,n by A3, A12
.= (log a,b) * (log b,n) by A5, A6, A12, POWER:64 ;
then t . n <= (c * (log a,b)) * (log b,n) by A14;
hence t . n <= (c * (log a,b)) * (g . n) by A4, A12; :: thesis: t . n >= 0
thus t . n >= 0 by A10, A13; :: thesis: verum

end;

hence x in Big_Oh g by A7, A11; :: 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
A15: x = t and
A16: 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
A17: c > 0 and
A18: for n being Element of NAT st n >= N holds
( t . n <= c * (g . n) & t . n >= 0 ) by A16;
log b,a > log b,1 by A1, A2, POWER:65;
then log b,a > 0 by A6, POWER:59;
then A19: c * (log b,a) > c * 0 by A17, XREAL_1:70;

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 A20: n >= N1 ; :: thesis: ( t . n <= (c * (log b,a)) * (f . n) & t . n >= 0 )
N + 1 > N + 0 by XREAL_1:10;
then A21: n > N by A20, XXREAL_0:2;
then A22: t . n <= c * (g . n) by A18;
g . n = log b,n by A4, A20
.= (log b,a) * (log a,n) by A5, A6, A20, POWER:64 ;
then t . n <= (c * (log b,a)) * (log a,n) by A22;
hence t . n <= (c * (log b,a)) * (f . n) by A3, A20; :: thesis: t . n >= 0
thus t . n >= 0 by A18, A21; :: thesis: verum

end;

hence x in Big_Oh f by A15, A19; :: thesis: verum

end;

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