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 )
set f = seq_n^ 8;
g is eventually-positive

proof

take 0 ; :: according to ASYMPT_0:def 6 :: 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 Lm27, POWER:39; :: 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 )
A2: seq_n^ 8 is Element of Funcs NAT ,REAL by FUNCT_2:11;
A3: g is Element of Funcs NAT ,REAL by FUNCT_2:11;

now

let n be Element of NAT ; :: thesis: ( n >= 1 implies ( g . n <= 1 * ((seq_n^ 8) . n) & g . n >= 0 ) )
assume A4: n >= 1 ; :: thesis: ( g . n <= 1 * ((seq_n^ 8) . n) & g . n >= 0 )
then A5: (seq_n^ 8) . n = n to_power (2 * 4) by Def3
.= (n to_power 2) to_power 4 by A4, POWER:38
.= (n ^2 ) to_power 4 by POWER:53 ;
A6: g . n = (((n ^2 ) - n) + 1) to_power 4 by A1;
((n ^2 ) - n) + 1 <= n ^2 by A4, Lm29;
hence g . n <= 1 * ((seq_n^ 8) . n) by A5, A6, Lm6, Lm27; :: thesis: g . n >= 0
thus g . n >= 0 by A6, Lm27, POWER:39; :: thesis: verum

end;

then A7: g in Big_Oh (seq_n^ 8) by A3;

now

let n be Element of NAT ; :: thesis: ( n >= 1 implies ( (seq_n^ 8) . n <= 16 * (g . n) & (seq_n^ 8) . n >= 0 ) )
assume A8: n >= 1 ; :: thesis: ( (seq_n^ 8) . n <= 16 * (g . n) & (seq_n^ 8) . n >= 0 )
then A9: (seq_n^ 8) . n = n to_power (2 * 4) by Def3
.= (n to_power 2) to_power 4 by A8, POWER:38
.= (n ^2 ) to_power 4 by POWER:53 ;
A10: g . n = (((n ^2 ) - n) + 1) to_power 4 by A1;
A11: n ^2 <= 2 * (((n ^2 ) - n) + 1) by A8, Lm30;
A12: ((n ^2 ) - n) + 1 > 0 by Lm27;
A13: n * n > n * 0 by A8, XREAL_1:70;
then (seq_n^ 8) . n <= (2 * (((n ^2 ) - n) + 1)) to_power 4 by A9, A11, Lm6;
hence (seq_n^ 8) . n <= 16 * (g . n) by A10, A12, Lm9, POWER:35; :: thesis: (seq_n^ 8) . n >= 0
thus (seq_n^ 8) . n >= 0 by A9, A13, POWER:39; :: thesis: verum

end;

then seq_n^ 8 in Big_Oh g by A2;
hence ( g = g & Big_Oh (seq_n^ 8) = Big_Oh g ) by A7, Lm5; :: thesis: verum