let d be XFinSequence of REAL ; :: thesis: for x, i being Nat st i in dom d holds
(d (#) (seq_a^ (x,1,0))) . i = (d . i) * (x to_power i)
let x, i be Nat; :: thesis: ( i in dom d implies (d (#) (seq_a^ (x,1,0))) . i = (d . i) * (x to_power i) )
assume i in dom d ; :: thesis: (d (#) (seq_a^ (x,1,0))) . i = (d . i) * (x to_power i)
hence (d (#) (seq_a^ (x,1,0))) . i = (d . i) * ((seq_a^ (x,1,0)) . i) by LMXFIN1
.= (d . i) * (x to_power ((1 * i) + 0)) by ASYMPT_1:def 1
.= (d . i) * (x to_power i) ;
:: thesis: verum