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