let X be Complex_Banach_Algebra; :: thesis: 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; :: thesis: 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; :: thesis: ( z,w are_commutative implies (1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n )

assume z,w are_commutative ; :: thesis: (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 ;

:: thesis: verum

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; :: thesis: 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; :: thesis: ( z,w are_commutative implies (1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n )

assume z,w are_commutative ; :: thesis: (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 ;

:: thesis: verum