defpred S₁[ Nat] means for c being nonnegative-yielding XFinSequence of REAL st len c = $1 + 1 holds
seq_p c in Big_Oh (seq_n^ $1);
P0: S₁[ 0 ] by LMXFIN6;
P1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume P11: S₁[k] ; :: thesis: S₁[k + 1]
let d be nonnegative-yielding XFinSequence of REAL ; :: thesis: ( len d = (k + 1) + 1 implies seq_p d in Big_Oh (seq_n^ (k + 1)) )
assume P12: len d = (k + 1) + 1 ; :: thesis: seq_p d in Big_Oh (seq_n^ (k + 1))
then consider a being Real, d1 being XFinSequence of REAL , y being Real_Sequence such that
P13: ( len d1 = k + 1 & d1 = d | (k + 1) & a = d . (k + 1) & d = d1 ^ <%a%> & seq_p d = (seq_p d1) + y & ( for i being Nat holds y . i = a * (i to_power (k + 1)) ) ) by LMXFIN4;
T11: for i being Nat st i in dom d1 holds
0 <= d1 . i

proof

let i be Nat; :: thesis: ( i in dom d1 implies 0 <= d1 . i )
assume AA1: i in dom d1 ; :: thesis: 0 <= d1 . i
then AA2: d1 . i = d . i by P13, FUNCT_1:47;
k + 1 <= (k + 1) + 1 by NAT_1:13;
then Segm (k + 1) c= Segm ((k + 1) + 1) by NAT_1:39;
hence 0 <= d1 . i by PARTFUN3:def 4, AA2, FUNCT_1:3, AA1, P12, P13; :: thesis: verum

end;

for r being Real st r in rng d1 holds
0 <= r

proof

let r be Real; :: thesis: ( r in rng d1 implies 0 <= r )
assume r in rng d1 ; :: thesis: 0 <= r
then consider x being object such that
RC: ( x in dom d1 & r = d1 . x ) by FUNCT_1:def 3;
thus 0 <= r by RC, T11; :: thesis: verum

end;

then d1 is nonnegative-yielding ;
then seq_p d1 in Big_Oh (seq_n^ k) by P11, P13;
then P14: seq_p d1 in Big_Oh (seq_n^ (k + 1)) by LMXFIN9, TARSKI:def 3;
k + 1 < (k + 1) + 1 by NAT_1:13;
then k + 1 in Segm ((k + 1) + 1) by NAT_1:44;
then d . (k + 1) in rng d by FUNCT_1:3, P12;
then y in Big_Oh (seq_n^ (k + 1)) by P13, LMXFIN8, PARTFUN3:def 4;
hence seq_p d in Big_Oh (seq_n^ (k + 1)) by P14, P13, LMXFIN7; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(P0, P1);
hence for k being Nat
for c being nonnegative-yielding XFinSequence of REAL st len c = k + 1 holds
seq_p c in Big_Oh (seq_n^ k) ; :: thesis: verum