let X be Complex_Banach_Algebra; :: thesis: for n being Element of NAT
for z, w being Element of X st z,w are_commutative holds
(1r / (n !c )) * ((z + w) #N n) = (Partial_Sums (Expan_e n,z,w)) . n
let n be Element of NAT ; :: thesis: for z, w being Element of X st z,w are_commutative holds
(1r / (n !c )) * ((z + w) #N n) = (Partial_Sums (Expan_e n,z,w)) . n
let z, w be Element of X; :: thesis: ( z,w are_commutative implies (1r / (n !c )) * ((z + w) #N n) = (Partial_Sums (Expan_e n,z,w)) . n )
assume A1: z,w are_commutative ; :: thesis: (1r / (n !c )) * ((z + w) #N n) = (Partial_Sums (Expan_e n,z,w)) . n
thus (1r / (n !c )) * ((z + w) #N n) = (1r / (n !c )) * ((Partial_Sums (Expan n,z,w)) . n) by A1, Th16
.= ((1r / (n !c )) * (Partial_Sums (Expan n,z,w))) . n by CLVECT_1:def 15
.= (Partial_Sums ((1r / (n !c )) * (Expan n,z,w))) . n by CLOPBAN3:23
.= (Partial_Sums (Expan_e n,z,w)) . n by Th17 ; :: thesis: verum