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 ;
A2: k -' k = 0 by A1, XREAL_1:235;
A3: (k -' k) !c = 1 by A1, Th1, XREAL_1:235;
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 !c ) * 1r )) * (z |^ k) by A3, Def11
.= ((z |^ k) * 1r ) / (k !c )
.= (z ExpSeq ) . k by Def8 ; :: thesis: verum