let f, g be eventually-nonnegative Real_Sequence; :: thesis: ( Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g iff ( f in Big_Oh g & not f in Big_Omega g ) )

hereby :: thesis: ( f in Big_Oh g & not f in Big_Omega g implies ( Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g ) )

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

now :: thesis: not f in Big_Omega g

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

end;

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

end;

assume that
A4: f in Big_Oh g and
A5: not f in Big_Omega g ; :: thesis: ( Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g )

now :: thesis: for x being object st x in Big_Oh f holds
x in Big_Oh g

let x be object ; :: thesis: ( x in Big_Oh f implies x in Big_Oh g )
assume x in Big_Oh f ; :: thesis: x in Big_Oh g
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: ex N being Nat st
for n being Nat st n >= N holds
t . n >= 0

reconsider N = N as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
t . n >= 0
let n be Nat; :: thesis: ( n >= N implies t . n >= 0 )
A9: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis: t . n >= 0
hence t . n >= 0 by A8, A9; :: thesis: verum

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: verum

end;

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