reconsider g = seq_a^ (2,1,1) as eventually-positive Real_Sequence ;
set f = seq_a^ (2,1,0);
take g ; :: thesis: ( g = seq_a^ (2,1,1) & seq_a^ (2,1,0) in Big_Theta g )
thus g = seq_a^ (2,1,1) ; :: thesis: seq_a^ (2,1,0) in Big_Theta g
A1: seq_a^ (2,1,0) is Element of Funcs (NAT,REAL) by FUNCT_2:8;

A2: now :: thesis: for n being Element of NAT st n >= 2 holds
( (2 to_power (- 1)) * (g . n) <= (seq_a^ (2,1,0)) . n & (seq_a^ (2,1,0)) . n <= 1 * (g . n) )

let n be Element of NAT ; :: thesis: ( n >= 2 implies ( (2 to_power (- 1)) * (g . n) <= (seq_a^ (2,1,0)) . n & (seq_a^ (2,1,0)) . n <= 1 * (g . n) ) )
assume n >= 2 ; :: thesis: ( (2 to_power (- 1)) * (g . n) <= (seq_a^ (2,1,0)) . n & (seq_a^ (2,1,0)) . n <= 1 * (g . n) )
A3: (seq_a^ (2,1,0)) . n = 2 to_power ((1 * n) + 0) by Def1;
A4: g . n = 2 to_power ((1 * n) + 1) by Def1;
then (2 to_power (- 1)) * (g . n) = 2 to_power ((- 1) + (n + 1)) by POWER:27
.= (seq_a^ (2,1,0)) . n by A3 ;
hence (2 to_power (- 1)) * (g . n) <= (seq_a^ (2,1,0)) . n ; :: thesis: (seq_a^ (2,1,0)) . n <= 1 * (g . n)
n + 0 <= n + 1 by XREAL_1:7;
hence (seq_a^ (2,1,0)) . n <= 1 * (g . n) by A3, A4, PRE_FF:8; :: thesis: verum

end;

A5: 2 to_power (- 1) > 0 by POWER:34;
Big_Theta g = { s where s is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (g . n) <= s . n & s . n <= c * (g . n) ) ) ) } by ASYMPT_0:27;
hence seq_a^ (2,1,0) in Big_Theta g by A1, A5, A2; :: thesis: verum