let X be 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) rExpSeq) by Def10
.= (Sum (z2 rExpSeq)) * (Sum (z1 rExpSeq)) by A1, Lm3
.= (exp z2) * (Sum (z1 rExpSeq)) by Def10
.= (exp z2) * (exp z1) by Def10 ;
exp (z1 + z2) = Sum ((z1 + z2) rExpSeq) by Def10
.= (Sum (z1 rExpSeq)) * (Sum (z2 rExpSeq)) by A1, Lm3
.= (exp z1) * (Sum (z2 rExpSeq)) by Def10
.= (exp z1) * (exp z2) by Def10 ;
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; :: thesis: verum