for X being Banach_Algebra
for z being Element of X
for s, t being Real holds s * z,t * z are_commutative