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:235;
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:43
.= ((Coef_e k) . k) * (z #N k) by CLOPBAN3:42
.= (1r / ((k !c) * 1r)) * (z #N k) by A1, COMPLEX1:def 7, SIN_COS:1, SIN_COS:def 11
.= (z ExpSeq) . k by Def2, COMPLEX1:def 7 ;
:: thesis: verum