set f = seq_n! 0 ;
set g = seq_n! 1;
set h = (seq_n! 0 ) /" (seq_n! 1);
A1: for n being Element of NAT holds ((seq_n! 0 ) /" (seq_n! 1)) . n = 1 / (n + 1)

proof

let n be Element of NAT ; :: thesis: ((seq_n! 0 ) /" (seq_n! 1)) . n = 1 / (n + 1)
A2: n ! <> 0 by NEWTON:23;
((seq_n! 0 ) /" (seq_n! 1)) . n = ((seq_n! 0 ) . n) / ((seq_n! 1) . n) by Lm4
.= ((n + 0 ) ! ) / ((seq_n! 1) . n) by Def5
.= (n ! ) / ((n + 1) ! ) by Def5
.= ((n ! ) * 1) / ((n + 1) * (n ! )) by NEWTON:21
.= (1 / (n + 1)) * ((n ! ) / (n ! )) by XCMPLX_1:77
.= (1 / (n + 1)) * 1 by A2, XCMPLX_1:60 ;
hence ((seq_n! 0 ) /" (seq_n! 1)) . n = 1 / (n + 1) ; :: 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_n! 0 ) /" (seq_n! 1)) . n) - 0 ) < 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_n! 0 ) /" (seq_n! 1)) . n) - 0 ) < p
then p " > 0 ;
then A5: 1 / p > 0 ;
set N = max 1,[/(1 / p)\];
A6: ( max 1,[/(1 / p)\] >= 1 & max 1,[/(1 / p)\] >= [/(1 / p)\] ) by XXREAL_0:25;
max 1,[/(1 / p)\] is Integer by XXREAL_0:16;
then reconsider N = max 1,[/(1 / p)\] as Element of NAT by A6, INT_1:16;
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs ((((seq_n! 0 ) /" (seq_n! 1)) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N implies abs ((((seq_n! 0 ) /" (seq_n! 1)) . n) - 0 ) < p )
assume n >= N ; :: thesis: abs ((((seq_n! 0 ) /" (seq_n! 1)) . n) - 0 ) < p
then A7: n + 1 > N by NAT_1:13;
A8: - p < - 0 by A4, XREAL_1:26;
0 < 1 / (n + 1) ;
then A9: - p < ((seq_n! 0 ) /" (seq_n! 1)) . n by A1, A8;
[/(1 / p)\] >= 1 / p by INT_1:def 5;
then N >= 1 / p by A6, XXREAL_0:2;
then n + 1 > 1 / p by A7, XXREAL_0:2;
then 1 / (n + 1) < 1 / (1 / p) by A5, XREAL_1:90;
then 1 / (n + 1) < p ;
then A10: ((seq_n! 0 ) /" (seq_n! 1)) . n < p by A1;
abs (((seq_n! 0 ) /" (seq_n! 1)) . n) < p

proof

per cases ( ((seq_n! 0 ) /" (seq_n! 1)) . n >= 0 or ((seq_n! 0 ) /" (seq_n! 1)) . n < 0 ) ;

suppose ((seq_n! 0 ) /" (seq_n! 1)) . n >= 0 ; :: thesis: abs (((seq_n! 0 ) /" (seq_n! 1)) . n) < p

hence abs (((seq_n! 0 ) /" (seq_n! 1)) . n) < p by A10, ABSVALUE:def 1; :: thesis: verum

end;

suppose ((seq_n! 0 ) /" (seq_n! 1)) . n < 0 ; :: thesis: abs (((seq_n! 0 ) /" (seq_n! 1)) . n) < p

then A11: abs (((seq_n! 0 ) /" (seq_n! 1)) . n) = - (((seq_n! 0 ) /" (seq_n! 1)) . n) by ABSVALUE:def 1;
(- 1) * (- p) > (- 1) * (((seq_n! 0 ) /" (seq_n! 1)) . n) by A9, XREAL_1:71;
hence abs (((seq_n! 0 ) /" (seq_n! 1)) . n) < p by A11; :: thesis: verum

end;

end;

end;

hence abs ((((seq_n! 0 ) /" (seq_n! 1)) . n) - 0 ) < p ; :: thesis: verum

end;

then A12: (seq_n! 0 ) /" (seq_n! 1) is convergent by SEQ_2:def 6;
then lim ((seq_n! 0 ) /" (seq_n! 1)) = 0 by A3, SEQ_2:def 7;
then ( seq_n! 0 in Big_Oh (seq_n! 1) & not seq_n! 1 in Big_Oh (seq_n! 0 ) ) by A12, ASYMPT_0:16;
then ( seq_n! 0 in Big_Oh (seq_n! 1) & not seq_n! 0 in Big_Omega (seq_n! 1) ) by ASYMPT_0:19;
hence ( Big_Oh (seq_n! 0 ) c= Big_Oh (seq_n! 1) & not Big_Oh (seq_n! 0 ) = Big_Oh (seq_n! 1) ) by Th4; :: thesis: verum