let X be Complex_Banach_Algebra; :: thesis: for z1, z2 being Element of X st z1,z2 are_commutative holds
( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative )
let z1, z2 be Element of X; :: thesis: ( z1,z2 are_commutative implies ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) )
assume A1: z1,z2 are_commutative ; :: thesis: ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative )
A2: exp (z2 + z1) = Sum ((z2 + z1) ExpSeq) by Def6
.= (Sum (z2 ExpSeq)) * (Sum (z1 ExpSeq)) by A1, Lm3
.= (exp z2) * (Sum (z1 ExpSeq)) by Def6
.= (exp z2) * (exp z1) by Def6 ;
exp (z1 + z2) = Sum ((z1 + z2) ExpSeq) by Def6
.= (Sum (z1 ExpSeq)) * (Sum (z2 ExpSeq)) by A1, Lm3
.= (exp z1) * (Sum (z2 ExpSeq)) by Def6
.= (exp z1) * (exp z2) by Def6 ;
hence ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) by A2, LOPBAN_4:def 1; :: thesis: verum