for f being eventually-nonnegative eventually-nondecreasing Real_Sequence
for t being Real_Sequence st ( for n being Element of NAT holds
( ( n mod 2 = 0 implies t . n = 1 ) & ( n mod 2 = 1 implies t . n = n ) ) ) holds
not t in Big_Theta f