let z, w be Element of COMPLEX ; :: thesis: for n being Element of NAT holds ((z + w) |^ n) / (n !c ) = (Partial_Sums (Expan_e n,z,w)) . n
let n be Element of NAT ; :: thesis: ((z + w) |^ n) / (n !c ) = (Partial_Sums (Expan_e n,z,w)) . n
thus ((z + w) |^ n) / (n !c ) = ((Partial_Sums (Expan n,z,w)) . n) * (1r / (n !c )) by Th7
.= ((1r / (n !c )) (#) (Partial_Sums (Expan n,z,w))) . n by VALUED_1:6
.= (Partial_Sums ((1r / (n !c )) (#) (Expan n,z,w))) . n by COMSEQ_3:29
.= (Partial_Sums (Expan_e n,z,w)) . n by Th8 ; :: thesis: verum