let w, z be Complex; :: 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
A1: 0 = k - k ;
then A2: k -' k = 0 by XREAL_1:233;
A3: (k -' k) ! = 1 by A1, Th1, XREAL_1:233;
thus (Expan_e (k,z,w)) . k = (((Coef_e k) . k) * (z |^ k)) * (w |^ 0) by A2, Def10
.= (((Coef_e k) . k) * (z |^ k)) * 1r by COMSEQ_3:11
.= (1r / ((k !) * 1r)) * (z |^ k) by A3, Def7
.= ((z |^ k) * 1r) / (k !)
.= (z ExpSeq) . k by Def4 ; :: thesis: verum