let X be Banach_Algebra; :: thesis: for n being Nat
for z, w being Element of X st z,w are_commutative holds
(1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n
let n be Nat; :: thesis: for z, w being Element of X st z,w are_commutative holds
(1 / (n !)) * ((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 (1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n )
assume z,w are_commutative ; :: thesis: (1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n
hence (1 / (n !)) * ((z + w) #N n) = (1 / (n !)) * ((Partial_Sums (Expan (n,z,w))) . n) by Th17
.= ((1 / (n !)) * (Partial_Sums (Expan (n,z,w)))) . n by NORMSP_1:def 5
.= (Partial_Sums ((1 / (n !)) * (Expan (n,z,w)))) . n by LOPBAN_3:19
.= (Partial_Sums (Expan_e (n,z,w))) . n by Th18 ;
:: thesis: verum