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
A1: ( s in COMPLEX & t in COMPLEX ) by XCMPLX_0:def 2;
then (s * z) * (t * z) = (s * t) * (z * z) by CLOPBAN3:38
.= (t * z) * (s * z) by A1, CLOPBAN3:38 ;
hence s * z,t * z are_commutative by LOPBAN_4:def 1; :: thesis: verum