set f = seq_a^ 2,1,0 ;
reconsider g = seq_a^ 2,1,1 as eventually-positive Real_Sequence ;
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: 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;
A2: seq_a^ 2,1,0 is Element of Funcs NAT ,REAL by FUNCT_2:11;
A3: 2 to_power (- 1) > 0 by POWER:39;

now

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) )
A4: (seq_a^ 2,1,0 ) . n = 2 to_power ((1 * n) + 0 ) by Def1;
A5: 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:32
.= (seq_a^ 2,1,0 ) . n by A4 ;
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:9;
hence (seq_a^ 2,1,0 ) . n <= 1 * (g . n) by A4, A5, PRE_FF:10; :: thesis: verum

end;

hence seq_a^ 2,1,0 in Big_Theta g by A1, A2, A3; :: thesis: verum