let X be Complex_Banach_Algebra; :: thesis: for z1, z2 being Element of X st z1,z2 are_commutative holds
z1 * (exp z2) = (exp z2) * z1
let z1, z2 be Element of X; :: thesis: ( z1,z2 are_commutative implies z1 * (exp z2) = (exp z2) * z1 )
assume A1: z1,z2 are_commutative ; :: thesis: z1 * (exp z2) = (exp z2) * z1

now

let n be Element of NAT ; :: thesis: (z1 * (z2 ExpSeq)) . n = ((z2 ExpSeq) * z1) . n
thus (z1 * (z2 ExpSeq)) . n = z1 * ((z2 ExpSeq) . n) by CLOPBAN3:def 4
.= z1 * ((1r / (n !)) * (z2 #N n)) by Def2
.= (1r / (n !)) * (z1 * (z2 #N n)) by CLOPBAN3:38
.= (1r / (n !)) * ((z2 #N n) * z1) by A1, Lm2
.= ((1r / (n !)) * (z2 #N n)) * z1 by CLOPBAN3:38
.= ((z2 ExpSeq) . n) * z1 by Def2
.= ((z2 ExpSeq) * z1) . n by CLOPBAN3:def 5 ; :: thesis: verum

end;

then A2: z1 * (z2 ExpSeq) = (z2 ExpSeq) * z1 by FUNCT_2:63;
A3: Partial_Sums (z2 ExpSeq) is convergent by CLOPBAN3:def 1;
thus z1 * (exp z2) = z1 * (Sum (z2 ExpSeq)) by Def8
.= z1 * (lim (Partial_Sums (z2 ExpSeq))) by CLOPBAN3:def 2
.= lim (z1 * (Partial_Sums (z2 ExpSeq))) by A3, Th6
.= lim (Partial_Sums (z1 * (z2 ExpSeq))) by Th9
.= lim ((Partial_Sums (z2 ExpSeq)) * z1) by A2, Th9
.= (lim (Partial_Sums (z2 ExpSeq))) * z1 by A3, Th7
.= (Sum (z2 ExpSeq)) * z1 by CLOPBAN3:def 2
.= (exp z2) * z1 by Def8 ; :: thesis: verum