let d be XFinSequence of REAL ; :: thesis: for k being Nat st len d = 1 holds

ex a being Real st

( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) )

let k be Nat; :: thesis: ( len d = 1 implies ex a being Real st

( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) ) )

assume AS: len d = 1 ; :: thesis: ex a being Real st

( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) )

reconsider a = d . 0 as Real ;

take a ; :: thesis: ( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) )

thus a = d . 0 ; :: thesis: for x being Nat holds (seq_p d) . x = a

let x be Nat; :: thesis: (seq_p d) . x = a

Q1: (seq_p d) . x = Sum (d (#) (seq_a^ (x,1,0))) by defseqp;

Q3: 0 in Segm 1 by NAT_1:44;

Q4: (d (#) (seq_a^ (x,1,0))) . 0 = (d . 0) * ((seq_a^ (x,1,0)) . 0) by AS, Q3, LMXFIN1

.= a * (x to_power ((1 * 0) + 0)) by ASYMPT_1:def 1

.= a * 1 by POWER:24

.= a ;

len (d (#) (seq_a^ (x,1,0))) = 1 by AS, LMXFIN1;

then d (#) (seq_a^ (x,1,0)) = <%a%> by AFINSQ_1:34, Q4;

hence (seq_p d) . x = a by Q1, AFINSQ_2:53; :: thesis: verum

ex a being Real st

( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) )

let k be Nat; :: thesis: ( len d = 1 implies ex a being Real st

( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) ) )

assume AS: len d = 1 ; :: thesis: ex a being Real st

( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) )

reconsider a = d . 0 as Real ;

take a ; :: thesis: ( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) )

thus a = d . 0 ; :: thesis: for x being Nat holds (seq_p d) . x = a

let x be Nat; :: thesis: (seq_p d) . x = a

Q1: (seq_p d) . x = Sum (d (#) (seq_a^ (x,1,0))) by defseqp;

Q3: 0 in Segm 1 by NAT_1:44;

Q4: (d (#) (seq_a^ (x,1,0))) . 0 = (d . 0) * ((seq_a^ (x,1,0)) . 0) by AS, Q3, LMXFIN1

.= a * (x to_power ((1 * 0) + 0)) by ASYMPT_1:def 1

.= a * 1 by POWER:24

.= a ;

len (d (#) (seq_a^ (x,1,0))) = 1 by AS, LMXFIN1;

then d (#) (seq_a^ (x,1,0)) = <%a%> by AFINSQ_1:34, Q4;

hence (seq_p d) . x = a by Q1, AFINSQ_2:53; :: thesis: verum