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_{1}[ Nat] means Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ (k + $1));

P0: S_{1}[ 0 ]
;

P1: for x being Nat st S_{1}[x] holds

S_{1}[x + 1]
_{1}[x]
from NAT_1:sch 2(P0, P1);

hence Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ n) by LA; :: thesis: verum

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

P0: S

P1: for x being Nat st S

S

proof

for x being Nat holds S
let x be Nat; :: thesis: ( S_{1}[x] implies S_{1}[x + 1] )

assume P1L1: S_{1}[x]
; :: thesis: S_{1}[x + 1]

Big_Oh (seq_n^ (k + x)) c= Big_Oh (seq_n^ ((k + x) + 1)) by LMXFIN9;

hence S_{1}[x + 1]
by XBOOLE_1:1, P1L1; :: thesis: verum

end;assume P1L1: S

Big_Oh (seq_n^ (k + x)) c= Big_Oh (seq_n^ ((k + x) + 1)) by LMXFIN9;

hence S

hence Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ n) by LA; :: thesis: verum