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:34
.= 2 to_power (0 + (- 1))
.= 1 / (2 to_power 1) by POWER:33
.= 1 / 2 by POWER:30
.= 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:7 ;
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