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 A1: ( Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g ) ; :: thesis: ( f in Big_Oh g & not f in Big_Omega g )
A2: 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, Lm5; :: thesis: verum

end;

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

end;

assume A3: ( f in Big_Oh g & 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
A4: x = t and
A5: 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
A6: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A5;

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 A6; :: thesis: verum

end;

then A7: t is eventually-nonnegative by ASYMPT_0:def 4;
t in Big_Oh f by A5;
hence x in Big_Oh g by A3, A4, A7, 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 ( f in Big_Oh g & g in Big_Oh f ) by Lm5;
hence contradiction by A3, ASYMPT_0:19; :: thesis: verum