let f be Real_Sequence; :: thesis:
assume A1: for n being Element of NAT holds f . n = Step1 n ; :: thesis:
set g = seq_n^ 1;
f is eventually-positive

proof

take 1 ; :: according to ASYMPT_0:def 6 :: thesis:
let n be Element of NAT ; :: thesis:
assume A2: n >= 1 ; :: thesis:
A3: f . n = Step1 n by A1;
consider m being Element of NAT such that
A4: ( m ! <= n & n < (m + 1) ! & Step1 n = m ! ) by A2, Def9;
thus not f . n <= 0 by A3, A4, NEWTON:23; :: thesis:

end;

then reconsider f = f as eventually-positive Real_Sequence ;
take f ; :: thesis:
A5: 1 = 2 - 1 ;

now

let k be Element of NAT ; :: thesis:
thus f . k <= f . (k + 1) :: thesis:

proof

per cases ;

suppose A6: k = 0 ; :: thesis:

A7: f . 0 = Step1 0 by A1
.= 0 by Def9 ;
f . (0 + 1) = Step1 1 by A1;
hence f . k <= f . (k + 1) by A6, A7; :: thesis:

end;

suppose A8: k > 0 ; :: thesis:

A9: k <= k + 1 by NAT_1:11;
consider n1 being Element of NAT such that
A10: ( n1 ! <= k & k < (n1 + 1) ! ) and
A11: Step1 k = n1 ! by A8, Def9;
A12: f . k = n1 ! by A1, A11;
A13: k + 1 <= (n1 + 1) ! by A10, INT_1:20;

per cases by A13, XXREAL_0:1;

suppose k + 1 < (n1 + 1) ! ; :: thesis:

then ( n1 ! <= k + 1 & k + 1 < (n1 + 1) ! ) by A9, A10, XXREAL_0:2;
then Step1 (k + 1) = n1 ! by Def9;
hence f . k <= f . (k + 1) by A1, A12; :: thesis:

end;

suppose A14: k + 1 = (n1 + 1) ! ; :: thesis:

A15: n1 + 2 > 0 + 1 by XREAL_1:10;
(n1 + 1) ! > 0 by NEWTON:23;
then 1 * ((n1 + 1) ! ) < (n1 + 2) * ((n1 + 1) ! ) by A15, XREAL_1:70;
then A16: k + 1 < ((n1 + 1) + 1) ! by A14, NEWTON:21;
f . (k + 1) = Step1 (k + 1) by A1
.= (n1 + 1) ! by A14, A16, Def9 ;
hence f . k <= f . (k + 1) by A12, Lm59, NAT_1:11; :: thesis:

end;

then A17: for k being Element of NAT st k >= 0 holds
f . k <= f . (k + 1) ;

A18: now

let n be Element of NAT ; :: thesis:
thus f . n <= (seq_n^ 1) . n :: thesis:

proof

per cases ;

suppose A19: n = 0 ; :: thesis:

f . 0 = Step1 0 by A1
.= 0 by Def9 ;
hence f . n <= (seq_n^ 1) . n by A19, Def3; :: thesis:

end;

suppose A20: n > 0 ; :: thesis:

then consider n1 being Element of NAT such that
A21: ( n1 ! <= n & n < (n1 + 1) ! ) and
A22: Step1 n = n1 ! by Def9;
(seq_n^ 1) . n = n to_power 1 by A20, Def3
.= n by POWER:30 ;
hence f . n <= (seq_n^ 1) . n by A1, A21, A22; :: thesis:

end;

now

assume A23: f is smooth ; :: thesis:
set h = f taken_every 2;
f is_smooth_wrt 2 by A23, ASYMPT_0:def 20;
then f taken_every 2 in Big_Oh f by ASYMPT_0:def 19;
then consider t being Element of Funcs NAT ,REAL such that
A24: t = f taken_every 2 and
A25: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
c > 0 and
A26: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A25;
set n2 = max (max N,3),([/c\] + 1);
A27: ( max (max N,3),([/c\] + 1) >= max N,3 & max (max N,3),([/c\] + 1) >= [/c\] + 1 ) by XXREAL_0:25;
A28: ( max N,3 >= N & max N,3 >= 3 ) by XXREAL_0:25;
then A29: ( max (max N,3),([/c\] + 1) >= N & max (max N,3),([/c\] + 1) >= 3 ) by A27, XXREAL_0:2;
max (max N,3),([/c\] + 1) is Integer by XXREAL_0:16;
then reconsider n2 = max (max N,3),([/c\] + 1) as Element of NAT by A27, INT_1:16;
set n1 = (n2 ! ) - 1;
A30: n2 > 2 by A29, XXREAL_0:2;
then A31: n2 ! >= 2 by Lm59, NEWTON:20;
then A32: (n2 ! ) - 1 >= 1 by A5, XREAL_1:11;
then reconsider n1 = (n2 ! ) - 1 as Element of NAT by INT_1:16;
set n3 = n2 - 1;
A33: n2 - 1 >= 1 by A5, A30, XREAL_1:11;
then reconsider n3 = n2 - 1 as Element of NAT by INT_1:16;
n2 ! > n2 by A29, Lm61;
then n2 ! >= n2 + 1 by INT_1:20;
then n1 >= n2 by XREAL_1:21;
then n1 >= N by A29, XXREAL_0:2;
then A34: t . n1 <= c * (f . n1) by A26;
A35: (n2 ! ) - 1 < (n2 ! ) - 0 by XREAL_1:17;
A36: n3 + 1 = n2 + 0 ;
then A37: n2 * (n3 ! ) = n2 ! by NEWTON:21;
A38: n3 ! >= 1 by A33, Lm59, NEWTON:19;
1 + 1 <= n2 by A29, XXREAL_0:2;
then 1 <= n2 - 1 by XREAL_1:21;
then 1 * 1 <= (n2 - 1) * (n3 ! ) by A38, Lm26;
then n2 * 1 <= ((n2 - 1) * (n3 ! )) * n2 by XREAL_1:66;
then n2 <= (n2 - 1) * ((n3 ! ) * (n3 + 1)) ;
then n2 <= (n2 - 1) * (n2 ! ) by NEWTON:21;
then (n2 ! ) + n2 <= ((n2 ! ) * 1) + ((n2 - 1) * (n2 ! )) by XREAL_1:8;
then n2 * (n3 ! ) <= (n2 * (n2 ! )) - n2 by A37, XREAL_1:21;
then n3 ! <= (n2 * ((n2 ! ) - 1)) / (n2 * 1) by A27, A28, XREAL_1:79;
then A39: n3 ! <= ((n2 ! ) - 1) / 1 by A27, A28, XCMPLX_1:92;
A40: f . n1 = Step1 n1 by A1
.= n3 ! by A32, A35, A36, A39, Def9 ;
A41: t . n1 = f . (2 * n1) by A24, ASYMPT_0:def 18;
A42: 2 * (n2 ! ) <= n2 * (n2 ! ) by A30, XREAL_1:66;
n2 < n2 + 1 by NAT_1:13;
then n2 * (n2 ! ) < (n2 + 1) * (n2 ! ) by A31, XREAL_1:70;
then n2 * (n2 ! ) < (n2 + 1) ! by NEWTON:21;
then A43: 2 * (n2 ! ) < (n2 + 1) ! by A42, XXREAL_0:2;
2 * n1 < 2 * (n2 ! ) by A35, XREAL_1:70;
then A44: 2 * n1 < (n2 + 1) ! by A43, XXREAL_0:2;
(n2 ! ) + 2 <= (n2 ! ) + (n2 ! ) by A31, XREAL_1:8;
then A45: n2 ! <= (2 * (n2 ! )) - (2 * 1) by XREAL_1:21;
A46: f . (2 * n1) = Step1 (2 * n1) by A1
.= (n3 + 1) ! by A31, A44, A45, Def9
.= n2 * (n3 ! ) by NEWTON:21 ;
A47: [/c\] + 1 > [/c\] + 0 by XREAL_1:10;
[/c\] >= c by INT_1:def 5;
then [/c\] + 1 > c by A47, XXREAL_0:2;
then A48: n2 > c by A27, XXREAL_0:2;
n3 ! > 0 by NEWTON:23;
hence contradiction by A34, A40, A41, A46, A48, XREAL_1:70; :: thesis:

end;

hence ( f = f & f is eventually-nondecreasing & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & not f is smooth ) by A17, A18, ASYMPT_0:def 8; :: thesis: