let f, g be eventually-nonnegative Real_Sequence; :: thesis:

hereby :: thesis:

assume that
A1: Big_Oh f c= Big_Oh g and
A2: not Big_Oh f = Big_Oh g ; :: thesis:
A3: f in Big_Oh f by ASYMPT_0:10;

now :: thesis:

assume f in Big_Omega g ; :: thesis:
then g in Big_Oh f by ASYMPT_0:19;
hence contradiction by A1, A2, A3, Lm5; :: thesis:

end;

hence ( f in Big_Oh g & not f in Big_Omega g ) by A1, A3; :: thesis:

end;

assume that
A4: f in Big_Oh g and
A5: not f in Big_Omega g ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in Big_Oh f ; :: thesis:
then consider t being Element of Funcs (NAT,REAL) such that
A6: x = t and
A7: 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
c > 0 and
A8: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A7;

now :: thesis:

reconsider N = N as Nat ;
take N = N; :: thesis:
let n be Nat; :: thesis:
A9: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis:
hence t . n >= 0 by A8, A9; :: thesis:

end;

then A10: t is eventually-nonnegative ;
t in Big_Oh f by A7;
hence x in Big_Oh g by A4, A6, A10, ASYMPT_0:12; :: thesis:

end;

hence Big_Oh f c= Big_Oh g by TARSKI:def 3; :: thesis:
assume Big_Oh f = Big_Oh g ; :: thesis:
then g in Big_Oh f by Lm5;
hence contradiction by A5, ASYMPT_0:19; :: thesis: