set g = seq_a^ (2,1,1);
set f = seq_a^ (2,1,0);
set h = (seq_a^ (2,1,0)) /" (seq_a^ (2,1,1));
reconsider f = seq_a^ (2,1,0) as eventually-positive Real_Sequence ;
reconsider g = seq_a^ (2,1,1) as eventually-positive Real_Sequence ;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = seq_a^ (2,1,0) & s1 = seq_a^ (2,1,1) & Big_Oh f = Big_Oh s1 )
take g ; :: thesis: ( f = seq_a^ (2,1,0) & g = seq_a^ (2,1,1) & Big_Oh f = Big_Oh g )
thus ( f = seq_a^ (2,1,0) & g = seq_a^ (2,1,1) ) ; :: thesis: Big_Oh f = Big_Oh g

A1: now

let n be Element of NAT ; :: thesis: ((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n = 2 "
A2: g . n = 2 to_power ((1 * n) + 1) by Def1;
f . n = 2 to_power ((1 * n) + 0) by Def1;
then ((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n = (2 to_power n) / (g . n) by Lm4
.= 2 to_power (n - (n + 1)) by A2, POWER:29
.= 2 to_power (0 + (- 1))
.= 1 / (2 to_power 1) by POWER:28
.= 1 / 2 by POWER:25
.= 2 " ;
hence ((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n = 2 " ; :: thesis: verum

end;

A3: now

let p be real number ; :: thesis: ( p > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")) < p )
assume A4: p > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")) < p
take N = 0 ; :: thesis: for n being Element of NAT st n >= N holds
abs ((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")) < p
let n be Element of NAT ; :: thesis: ( n >= N implies abs ((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")) < p )
assume n >= N ; :: thesis: abs ((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")) < p
abs ((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")) = abs ((2 ") - (2 ")) by A1
.= 0 by ABSVALUE:2 ;
hence abs ((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")) < p by A4; :: thesis: verum

end;

then A5: (seq_a^ (2,1,0)) /" (seq_a^ (2,1,1)) is convergent by SEQ_2:def 6;
then lim ((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) > 0 by A3, SEQ_2:def 7;
hence Big_Oh f = Big_Oh g by A5, ASYMPT_0:15; :: thesis: verum