( f in Big_Oh f & f in Big_Omega f ) by Th10, Th20;
then A1: not (Big_Oh f) /\ (Big_Omega f) is empty by XBOOLE_0:def 4;

now

let x be set ; :: thesis: ( x in (Big_Oh f) /\ (Big_Omega f) implies x is Function )
assume x in (Big_Oh f) /\ (Big_Omega f) ; :: thesis: x is Function
then x in Big_Oh f by XBOOLE_0:def 4;
then ex t being Element of Funcs NAT ,REAL st
( x = t & 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 ) ) ) ) ;
hence x is Function ; :: thesis: verum

end;

then A2: (Big_Oh f) /\ (Big_Omega f) is functional by FRAENKEL:def 1;

now

let x be Element of (Big_Oh f) /\ (Big_Omega f); :: thesis: x is Function of NAT , REAL
x in Big_Oh f by A1, XBOOLE_0:def 4;
hence x is Function of NAT , REAL by Th6; :: thesis: verum

end;

hence (Big_Oh f) /\ (Big_Omega f) is FUNCTION_DOMAIN of NAT , REAL by A1, A2, FRAENKEL:def 2; :: thesis: verum