for f, g being Real_Sequence st ( for n being Element of NAT st n > 0 holds
g . n = n * (log (2,n)) ) & ( for n being Nat holds f . n = log (2,(n !)) ) holds
ex s being eventually-nonnegative Real_Sequence st
( s = g & f in Big_Theta s )