let k, n be Nat; :: thesis: ( k <= n implies Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ n) )
assume k <= n ; :: thesis: Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ n)
then consider i being Nat such that
LA: n = k + i by NAT_1:10;
defpred S₁[ Nat] means Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ (k + $1));
P0: S₁[ 0 ] ;
P1: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume P1L1: S₁[x] ; :: thesis: S₁[x + 1]
Big_Oh (seq_n^ (k + x)) c= Big_Oh (seq_n^ ((k + x) + 1)) by LMXFIN9;
hence S₁[x + 1] by XBOOLE_1:1, P1L1; :: thesis: verum

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(P0, P1);
hence Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ n) by LA; :: thesis: verum