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