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 ( f in Big_Oh g & g in Big_Oh f ) ; :: thesis: Big_Oh f = Big_Oh g
then ( Big_Oh f c= Big_Oh g & Big_Oh g c= Big_Oh f ) by Th11;
hence Big_Oh f = Big_Oh g by XBOOLE_0:def 10; :: thesis: verum

end;

assume Big_Oh f = Big_Oh g ; :: thesis: ( f in Big_Oh g & g in Big_Oh f )
hence ( f in Big_Oh g & g in Big_Oh f ) by Th10; :: thesis: verum