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

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 5;
then [/((N + 1) / d)\] + 1 >= ((N + 1) / d) + 1 by XREAL_1:8;
then A6: d * ([/((N + 1) / d)\] + 1) >= d * (((N + 1) / d) + 1) by A4, XREAL_1:66;
A7: N + 1 >= 1 + 0 by XREAL_1:8;
d * (((N + 1) / d) + 1) = (d * ((N + 1) / d)) + (d * 1)
.= (N + 1) + d by A4, XCMPLX_1:88 ;
then A8: d * (((N + 1) / d) + 1) > 1 by A4, A7, XREAL_1:10;
take n = max N,[/((N + 1) / d)\]; :: thesis: ( n is Element of REAL & 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:16;
A11: n ! <> 0 by NEWTON:23;
n + 1 >= [/((N + 1) / d)\] + 1 by A10, XREAL_1:8;
then d * (n + 1) >= d * ([/((N + 1) / d)\] + 1) by A4, XREAL_1:66;
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 Def5
.= 1 by A11, XCMPLX_0:def 7 ;
(d * ((seq_n! 1) . n)) * ((n ! ) " ) = (d * ((n + 1) ! )) * ((n ! ) " ) by Def5
.= (d * ((n + 1) * (n ! ))) * ((n ! ) " ) by NEWTON:21
.= (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 Element of REAL & n is Element of NAT & n >= N & d * ((seq_n! 1) . n) > (seq_n! 0 ) . n ) by A13, XREAL_1:66, 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