let X be Complex_Banach_Algebra; for n being Nat
for z, w being Element of X st z,w are_commutative holds
(1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n
let n be Nat; for z, w being Element of X st z,w are_commutative holds
(1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n
let z, w be Element of X; ( z,w are_commutative implies (1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n )
assume
z,w are_commutative
; (1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n
hence (1r / (n !)) * ((z + w) #N n) =
(1r / (n !)) * ((Partial_Sums (Expan (n,z,w))) . n)
by Th16
.=
((1r / (n !)) * (Partial_Sums (Expan (n,z,w)))) . n
by CLVECT_1:def 14
.=
(Partial_Sums ((1r / (n !)) * (Expan (n,z,w)))) . n
by CLOPBAN3:19
.=
(Partial_Sums (Expan_e (n,z,w))) . n
by Th17
;
verum