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:17;
((seq_n! 0) /" (seq_n! 1)) . n = ((seq_n! 0) . n) / ((seq_n! 1) . n) by Lm4
.= ((n + 0) !) / ((seq_n! 1) . n) by Def4
.= (n !) / ((n + 1) !) by Def4
.= ((n !) * 1) / ((n + 1) * (n !)) by NEWTON:15
.= (1 / (n + 1)) * ((n !) / (n !)) by XCMPLX_1:76
.= (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 :: thesis: for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < p

let p be Real; :: thesis: ( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < p )
assume A4: p > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.((((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:3;
[/(1 / p)\] >= 1 / p by INT_1:def 7;
then A7: N >= 1 / p by A6, XXREAL_0:2;
reconsider N = N as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
|.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N implies |.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < p )
A8: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis: |.((((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:88;
then A9: ((seq_n! 0) /" (seq_n! 1)) . n < p by A1, A8;
A10: 0 < 1 / (n + 1) ;
- p < - 0 by A4, XREAL_1:24;
then A11: - p < ((seq_n! 0) /" (seq_n! 1)) . n by A1, A10, A8;
|.(((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: |.(((seq_n! 0) /" (seq_n! 1)) . n).| < p

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

end;

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

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

end;

end;

end;

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

end;

then A14: (seq_n! 0) /" (seq_n! 1) is convergent by SEQ_2:def 6;
then A15: 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 A14, ASYMPT_0:16;
then A16: not seq_n! 0 in Big_Omega (seq_n! 1) by ASYMPT_0:19;
seq_n! 0 in Big_Oh (seq_n! 1) by A14, A15, ASYMPT_0:16;
hence ( Big_Oh (seq_n! 0) c= Big_Oh (seq_n! 1) & Big_Oh (seq_n! 0) <> Big_Oh (seq_n! 1) ) by A16, Th4; :: thesis: verum