let k be Nat; :: thesis: Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ (k + 1))
set g = seq_n^ (k + 1);
set f = seq_n^ k;
A0: k < k + 1 by NAT_1:13;

A1: now :: thesis: for n being Element of NAT st n >= 2 holds
( (seq_n^ k) . n <= 1 * ((seq_n^ (k + 1)) . n) & (seq_n^ k) . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= 2 implies ( (seq_n^ k) . n <= 1 * ((seq_n^ (k + 1)) . n) & (seq_n^ k) . n >= 0 ) )
assume A2: n >= 2 ; :: thesis: ( (seq_n^ k) . n <= 1 * ((seq_n^ (k + 1)) . n) & (seq_n^ k) . n >= 0 )
then A3: n > 1 by XXREAL_0:2;
A4: (seq_n^ k) . n = n to_power k by A2, ASYMPT_1:def 3;
(seq_n^ (k + 1)) . n = n to_power (k + 1) by A2, ASYMPT_1:def 3;
hence (seq_n^ k) . n <= 1 * ((seq_n^ (k + 1)) . n) by A3, A4, A0, POWER:39; :: thesis: (seq_n^ k) . n >= 0
thus (seq_n^ k) . n >= 0 by A4; :: thesis: verum

end;

seq_n^ k is Element of Funcs (NAT,REAL) by FUNCT_2:8;
then seq_n^ k in Big_Oh (seq_n^ (k + 1)) by A1;
hence Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ (k + 1)) by ASYMPT_0:11; :: thesis: verum