set g = seq_n! 1;
set f = seq_n! 0 ;
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
set N = max 1,[/(1 / p)\];
A5: max 1,[/(1 / p)\] >= 1 by XXREAL_0:25;
A6: 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 A5, INT_1:16;
[/(1 / p)\] >= 1 / p by INT_1:def 5;
then A7: N >= 1 / p by A6, XXREAL_0:2;
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 n + 1 > N by NAT_1:13;
then n + 1 > 1 / p by A7, XXREAL_0:2;
then 1 / (n + 1) < 1 / (1 / p) by A4, XREAL_1:90;
then A8: ((seq_n! 0 ) /" (seq_n! 1)) . n < p by A1;
A9: 0 < 1 / (n + 1) ;
- p < - 0 by A4, XREAL_1:26;
then A10: - p < ((seq_n! 0 ) /" (seq_n! 1)) . n by A1, A9;
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 A8, ABSVALUE:def 1; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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