let X be Banach_Algebra; :: thesis: for z being Element of X
for s, t being Real holds s * z,t * z are_commutative
let z be Element of X; :: thesis: for s, t being Real holds s * z,t * z are_commutative
let s, t be Real; :: thesis: s * z,t * z are_commutative
(s * z) * (t * z) = (s * t) * (z * z) by LOPBAN_3:38
.= (t * z) * (s * z) by LOPBAN_3:38 ;
hence s * z,t * z are_commutative by Def1; :: thesis: verum