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

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

assume that
A1: f in Big_Oh g and
A2: g in Big_Oh f ; :: thesis: Big_Oh f = Big_Oh g
A3: Big_Oh g c= Big_Oh f by A2, ASYMPT_0:11;
Big_Oh f c= Big_Oh g by A1, ASYMPT_0:11;
hence Big_Oh f = Big_Oh g by A3, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( Big_Oh f = Big_Oh g implies ( f in Big_Oh g & g in Big_Oh f ) ) by ASYMPT_0:10; :: thesis: verum