let k be Nat; :: thesis: for c being XFinSequence of REAL st len c = k + 1 & 0 < c . k holds

seq_p c is polynomially-bounded

let c be XFinSequence of REAL ; :: thesis: ( len c = k + 1 & 0 < c . k implies seq_p c is polynomially-bounded )

assume AS: ( len c = k + 1 & 0 < c . k ) ; :: thesis: seq_p c is polynomially-bounded

take k ; :: according to ASYMPT_2:def 1 :: thesis: seq_p c in Big_Oh (seq_n^ k)

thus seq_p c in Big_Oh (seq_n^ k) by LMXFIN20A, TLNEG3, AS; :: thesis: verum

seq_p c is polynomially-bounded

let c be XFinSequence of REAL ; :: thesis: ( len c = k + 1 & 0 < c . k implies seq_p c is polynomially-bounded )

assume AS: ( len c = k + 1 & 0 < c . k ) ; :: thesis: seq_p c is polynomially-bounded

take k ; :: according to ASYMPT_2:def 1 :: thesis: seq_p c in Big_Oh (seq_n^ k)

thus seq_p c in Big_Oh (seq_n^ k) by LMXFIN20A, TLNEG3, AS; :: thesis: verum