( 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 :: thesis: for x being Element of (Big_Oh f) /\ (Big_Omega f) holds x is sequence of REAL

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

end;

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