defpred S_{1}[ 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_{1}[ 0 ]
by LMXFIN6;

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

S_{1}[k + 1]
_{1}[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

seq_p c in Big_Oh (seq_n^ $1);

P0: S

P1: for k being Nat st S

S

proof

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

assume P11: S_{1}[k]
; :: thesis: S_{1}[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

0 <= r

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;assume P11: S

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

for r being Real st r in rng d1 holds
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;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

0 <= r

proof

then
d1 is nonnegative-yielding
;
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;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

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

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