for t, t1 being Real_Sequence st t . 0 = 0 & ( for n being Element of NAT st n > 0 holds
t . n = ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 ) & ( for n being Element of NAT st n > 0 holds
t1 . n = (n to_power 3) * (log (2,n)) ) holds
ex s, s1 being eventually-positive Real_Sequence st
( s = t & s1 = t1 & s in Big_Oh s1 )