let X be Complex_Banach_Algebra; :: thesis: for w, z being Element of X
for k being Nat holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k
let w, z be Element of X; :: thesis: for k being Nat holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k
let k be Nat; :: thesis: (z ExpSeq) . k = (Expan_e (k,z,w)) . k
0 = k - k ;
then A1: k -' k = 0 by XREAL_1:233;
hence (Expan_e (k,z,w)) . k = (((Coef_e k) . k) * (z #N k)) * (w #N 0) by Def3
.= (((Coef_e k) . k) * (z #N k)) * (1. X) by CLOPBAN3:39
.= ((Coef_e k) . k) * (z #N k) by VECTSP_1:def 4
.= (1r / ((k !) * 1r)) * (z #N k) by A1, COMPLEX1:def 4, SIN_COS:1, SIN_COS:def 7
.= (z ExpSeq) . k by Def1, COMPLEX1:def 4 ;
:: thesis: verum