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

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

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

take N = N; :: thesis: for n being Element of NAT st n >= N holds
t . n >= 0
let n be Element of NAT ; :: thesis: ( n >= N implies t . n >= 0 )
assume n >= N ; :: thesis: t . n >= 0
hence t . n >= 0 by A8; :: thesis: verum

end;

then A9: t is eventually-nonnegative by ASYMPT_0:def 2;
t in Big_Oh f by A7;
hence x in Big_Oh g by A4, A6, A9, 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