defpred S₁[ Nat] means for c being non empty positive-yielding XFinSequence of REAL st len c = $1 holds
for x being Nat holds 0 < (polynom c) . x;
P0: S₁[ 0 ] ;
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 A1: S₁[k] ; :: thesis: S₁[k + 1]
let d be non empty positive-yielding XFinSequence of REAL ; :: thesis: ( len d = k + 1 implies for x being Nat holds 0 < (polynom d) . x )
assume A2: len d = k + 1 ; :: thesis: for x being Nat holds 0 < (polynom d) . x
then consider a being Real, d1 being XFinSequence of REAL , y being Real_Sequence such that
A3: ( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> & polynom d = (polynom d1) + y & ( for i being Nat holds y . i = a * (i to_power k) ) ) by ASYMPT_2:28;

per cases ( k = 0 or k <> 0 ) ;

suppose X1: k = 0 ; :: thesis: for x being Nat holds 0 < (polynom d) . x

then consider a being Real such that
A4: ( a = d . 0 & ( for x being Nat holds (polynom d) . x = a ) ) by ASYMPT_2:29, A2;
0 in Segm (0 + 1) by NAT_1:44;
then d . 0 in rng d by FUNCT_1:3, X1, A2;
then A5: 0 < d . 0 by PARTFUN3:def 1;
let x be Nat; :: thesis: 0 < (polynom d) . x
reconsider n = x as Nat ;
thus 0 < (polynom d) . x by A5, A4; :: thesis: verum

end;

suppose A7: k <> 0 ; :: thesis: for x being Nat holds 0 < (polynom d) . x

now :: thesis: for r being Real st r in rng d1 holds
0 < r

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
P4: ( x in dom d1 & r = d1 . x ) by FUNCT_1:def 3;
P5: d1 . x = d . x by P4, A3, FUNCT_1:47;
x in dom d by P4, A3, RELAT_1:60, TARSKI:def 3;
then d . x in rng d by FUNCT_1:3;
hence 0 < r by PARTFUN3:def 1, P5, P4; :: thesis: verum

end;

then A8: d1 is positive-yielding ;
reconsider d1 = d1 as non empty positive-yielding XFinSequence of REAL by A7, A8, A3;
let x be Nat; :: thesis: 0 < (polynom d) . x
reconsider n = x as Nat ;
A9: 0 < (polynom d1) . n by A1, A3;
A10: (polynom d) . n = ((polynom d1) . n) + (y . n) by SEQ_1:7, A3;
A11: y . n = a * (n to_power k) by A3;
k < k + 1 by NAT_1:13;
then k in Segm (k + 1) by NAT_1:44;
then d . k in rng d by FUNCT_1:3, A2;
then 0 < d . k by PARTFUN3:def 1;
hence 0 < (polynom d) . x by A10, A9, A11, A3; :: thesis: verum

end;

end;

end;

P2: for k being Nat holds S₁[k] from NAT_1:sch 2(P0, P1);
let c be non empty positive-yielding XFinSequence of REAL ; :: thesis: for x being Nat holds 0 < (polynom c) . x
let x be Nat; :: thesis: 0 < (polynom c) . x
len c is Nat ;
hence 0 < (polynom c) . x by P2; :: thesis: verum