let X be Banach_Algebra; :: thesis: for z being Element of X
for s, t being Real holds
( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative )
let z be Element of X; :: thesis: for s, t being Real holds
( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative )
let s, t be Real; :: thesis: ( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative )
A1: s * z,t * z are_commutative by Th40;
hence A2: (exp (s * z)) * (exp (t * z)) = exp ((s * z) + (t * z)) by Th35
.= exp ((s + t) * z) by LOPBAN_3:38 ;
:: thesis: ( (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative )
thus A3: (exp (t * z)) * (exp (s * z)) = exp ((t * z) + (s * z)) by A1, Th35
.= exp ((t + s) * z) by LOPBAN_3:38 ; :: thesis: ( exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative )
thus exp ((s + t) * z) = exp ((t + s) * z) ; :: thesis: exp (s * z), exp (t * z) are_commutative
thus exp (s * z), exp (t * z) are_commutative by A2, A3; :: thesis: verum