let X be Complex_Banach_Algebra; :: thesis: for z, w being Element of X
for k being Element of NAT holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k
let z, w be Element of X; :: thesis: for k being Element of NAT holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k
let k be Element of 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 Def5
.= (((Coef_e k) . k) * (z #N k)) * (1. X) by CLOPBAN3:39
.= ((Coef_e k) . k) * (z #N k) by CLOPBAN3:38
.= (1r / ((k !) * 1r)) * (z #N k) by A1, COMPLEX1:def 4, SIN_COS:1, SIN_COS:def 7
.= (z ExpSeq) . k by Def2, COMPLEX1:def 4 ;
:: thesis: verum