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