let r be Real; :: thesis: ( 0 < r implies ex c being non empty positive-yielding XFinSequence of REAL st
for x being Nat holds (polynom c) . x = r )
assume AS: 0 < r ; :: thesis: ex c being non empty positive-yielding XFinSequence of REAL st
for x being Nat holds (polynom c) . x = r
r is Element of REAL by XREAL_0:def 1;
then reconsider z = <%r%> as XFinSequence of REAL ;

now :: thesis: for x being Real st x in rng z holds
0 < x

let x be Real; :: thesis: ( x in rng z implies 0 < x )
assume x in rng z ; :: thesis: 0 < x
then x in {r} by AFINSQ_1:33;
hence 0 < x by AS, TARSKI:def 1; :: thesis: verum

end;

then A1: z is positive-yielding ;
reconsider z = z as non empty positive-yielding XFinSequence of REAL by A1;
take z ; :: thesis: for x being Nat holds (polynom z) . x = r
len z = 1 by AFINSQ_1:34;
then consider a being Real such that
A2: ( a = z . 0 & ( for x being Nat holds (seq_p z) . x = a ) ) by ASYMPT_2:29;
thus for x being Nat holds (polynom z) . x = r by A2; :: thesis: verum