for X being Banach_Algebra
for z being Element of X
for s, t being Real holds
( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative )