let z, w be Element of COMPLEX ; :: 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
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, Def14
.= (((Coef_e k) . k) * (z |^ k)) * 1r by COMSEQ_3:11
.= (1r / ((k !) * 1r)) * (z |^ k) by A3, Def11
.= ((z |^ k) * 1r) / (k !)
.= (z ExpSeq) . k by Def8 ; :: thesis: verum