for X being Banach_Algebra
for z1, z2 being Element of X st z1,z2 are_commutative holds
z1 * (exp z2) = (exp z2) * z1