for X being Complex_Banach_Algebra
for z being Element of X
for s, t being Complex holds s * z,t * z are_commutative