set g = seq_n! 1;
set f = seq_n! 0;
A1: Big_Theta (seq_n! 1) = { s where s is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((seq_n! 1) . n) <= s . n & s . n <= c * ((seq_n! 1) . n) ) ) ) } by ASYMPT_0:27;

now :: thesis: not seq_n! 0 in Big_Theta (seq_n! 1)

assume seq_n! 0 in Big_Theta (seq_n! 1) ; :: thesis: contradiction
then consider s being Element of Funcs (NAT,REAL) such that
A2: s = seq_n! 0 and
A3: ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((seq_n! 1) . n) <= s . n & s . n <= c * ((seq_n! 1) . n) ) ) ) by A1;
consider c, d being Real, N being Element of NAT such that
c > 0 and
A4: d > 0 and
A5: for n being Element of NAT st n >= N holds
( d * ((seq_n! 1) . n) <= s . n & s . n <= c * ((seq_n! 1) . n) ) by A3;
ex n being Element of NAT st
( n >= N & d * ((seq_n! 1) . n) > (seq_n! 0) . n )

proof

[/((N + 1) / d)\] >= (N + 1) / d by INT_1:def 7;
then [/((N + 1) / d)\] + 1 >= ((N + 1) / d) + 1 by XREAL_1:6;
then A6: d * ([/((N + 1) / d)\] + 1) >= d * (((N + 1) / d) + 1) by A4, XREAL_1:64;
A7: N + 1 >= 1 + 0 by XREAL_1:6;
d * (((N + 1) / d) + 1) = (d * ((N + 1) / d)) + (d * 1)
.= (N + 1) + d by A4, XCMPLX_1:87 ;
then A8: d * (((N + 1) / d) + 1) > 1 by A4, A7, XREAL_1:8;
take n = max (N,[/((N + 1) / d)\]); :: thesis: ( n is set & n is Element of NAT & n >= N & d * ((seq_n! 1) . n) > (seq_n! 0) . n )
A9: n >= N by XXREAL_0:25;
A10: n >= [/((N + 1) / d)\] by XXREAL_0:25;
n is Integer by XXREAL_0:16;
then reconsider n = n as Element of NAT by A9, INT_1:3;
A11: n ! <> 0 by NEWTON:17;
n + 1 >= [/((N + 1) / d)\] + 1 by A10, XREAL_1:6;
then d * (n + 1) >= d * ([/((N + 1) / d)\] + 1) by A4, XREAL_1:64;
then A12: d * (n + 1) >= d * (((N + 1) / d) + 1) by A6, XXREAL_0:2;
A13: ((seq_n! 0) . n) * ((n !) ") = ((n + 0) !) * ((n !) ") by Def4
.= 1 by A11, XCMPLX_0:def 7 ;
(d * ((seq_n! 1) . n)) * ((n !) ") = (d * ((n + 1) !)) * ((n !) ") by Def4
.= (d * ((n + 1) * (n !))) * ((n !) ") by NEWTON:15
.= (d * (n + 1)) * ((n !) * ((n !) "))
.= (d * (n + 1)) * 1 by A11, XCMPLX_0:def 7
.= d * (n + 1) ;
then (d * ((seq_n! 1) . n)) * ((n !) ") > 1 by A12, A8, XXREAL_0:2;
hence ( n is set & n is Element of NAT & n >= N & d * ((seq_n! 1) . n) > (seq_n! 0) . n ) by A13, XREAL_1:64, XXREAL_0:25; :: thesis: verum

end;

hence contradiction by A2, A5; :: thesis: verum

end;

hence not seq_n! 0 in Big_Theta (seq_n! 1) ; :: thesis: verum