set g = seq_n^ (1 / 2);
set f = seq_logn ;
A1: lim (seq_logn /" (seq_n^ (1 / 2))) = 0 by Lm11;
A2: seq_logn /" (seq_n^ (1 / 2)) is convergent by Lm11;
then not seq_n^ (1 / 2) in Big_Oh seq_logn by A1, ASYMPT_0:16;
then A3: not seq_logn in Big_Omega (seq_n^ (1 / 2)) by ASYMPT_0:19;
seq_logn in Big_Oh (seq_n^ (1 / 2)) by A2, A1, ASYMPT_0:16;
hence ( Big_Oh seq_logn c= Big_Oh (seq_n^ (1 / 2)) & not Big_Oh seq_logn = Big_Oh (seq_n^ (1 / 2)) ) by A3, Th4; :: thesis: verum