let X be Complex_Banach_Algebra; :: thesis: for z being Element of X
for s, t being Complex holds s * z,t * z are_commutative
let z be Element of X; :: thesis: for s, t being Complex holds s * z,t * z are_commutative
let s, t be Complex; :: thesis: s * z,t * z are_commutative
(s * z) * (t * z) = (s * t) * (z * z) by CLOPBAN3:38
.= (t * z) * (s * z) by CLOPBAN3:38 ;
hence s * z,t * z are_commutative by LOPBAN_4:def 1; :: thesis: verum