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