let g be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds g . n = (((n ^2) - n) + 1) to_power 4 ) implies ex s being eventually-positive Real_Sequence st
( s = g & Big_Oh (seq_n^ 8) = Big_Oh s ) )
assume A1: for n being Element of NAT holds g . n = (((n ^2) - n) + 1) to_power 4 ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = g & Big_Oh (seq_n^ 8) = Big_Oh s )
g is eventually-positive

proof

take 0 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being Element of NAT holds
( not 0 <= b₁ or not g . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 0 <= n or not g . n <= 0 )
assume n >= 0 ; :: thesis: not g . n <= 0
g . n = (((n ^2) - n) + 1) to_power 4 by A1;
hence not g . n <= 0 by Lm21, POWER:34; :: thesis: verum

end;

then reconsider g = g as eventually-positive Real_Sequence ;
take g ; :: thesis: ( g = g & Big_Oh (seq_n^ 8) = Big_Oh g )
set f = seq_n^ 8;

A2: now

let n be Element of NAT ; :: thesis: ( n >= 1 implies ( g . n <= 1 * ((seq_n^ 8) . n) & g . n >= 0 ) )
A3: g . n = (((n ^2) - n) + 1) to_power 4 by A1;
assume A4: n >= 1 ; :: thesis: ( g . n <= 1 * ((seq_n^ 8) . n) & g . n >= 0 )
then A5: ((n ^2) - n) + 1 <= n ^2 by Lm23;
(seq_n^ 8) . n = n to_power (2 * 4) by A4, Def3
.= (n to_power 2) to_power 4 by A4, POWER:33
.= (n ^2) to_power 4 by POWER:46 ;
hence g . n <= 1 * ((seq_n^ 8) . n) by A3, A5, Lm6, Lm21; :: thesis: g . n >= 0
thus g . n >= 0 by A3, Lm21, POWER:34; :: thesis: verum

end;

A6: now

let n be Element of NAT ; :: thesis: ( n >= 1 implies ( (seq_n^ 8) . n <= 16 * (g . n) & (seq_n^ 8) . n >= 0 ) )
A7: g . n = (((n ^2) - n) + 1) to_power 4 by A1;
A8: ((n ^2) - n) + 1 > 0 by Lm21;
assume A9: n >= 1 ; :: thesis: ( (seq_n^ 8) . n <= 16 * (g . n) & (seq_n^ 8) . n >= 0 )
then A10: (seq_n^ 8) . n = n to_power (2 * 4) by Def3
.= (n to_power 2) to_power 4 by A9, POWER:33
.= (n ^2) to_power 4 by POWER:46 ;
A11: n * n > n * 0 by A9, XREAL_1:68;
n ^2 <= 2 * (((n ^2) - n) + 1) by A9, Lm24;
then (seq_n^ 8) . n <= (2 * (((n ^2) - n) + 1)) to_power 4 by A10, A11, Lm6;
hence (seq_n^ 8) . n <= 16 * (g . n) by A7, A8, POWER:30, POWER:62; :: thesis: (seq_n^ 8) . n >= 0
thus (seq_n^ 8) . n >= 0 by A10, A11, POWER:34; :: thesis: verum

end;

seq_n^ 8 is Element of Funcs (NAT,REAL) by FUNCT_2:8;
then A12: seq_n^ 8 in Big_Oh g by A6;
g is Element of Funcs (NAT,REAL) by FUNCT_2:8;
then g in Big_Oh (seq_n^ 8) by A2;
hence ( g = g & Big_Oh (seq_n^ 8) = Big_Oh g ) by A12, Lm5; :: thesis: verum