let X be Banach_Algebra; :: thesis: for z1, z2 being Element of X st z1,z2 are_commutative holds
z1 * (exp z2) = (exp z2) * z1
let z1, z2 be Element of X; :: thesis: ( z1,z2 are_commutative implies z1 * (exp z2) = (exp z2) * z1 )
assume A1: z1,z2 are_commutative ; :: thesis: z1 * (exp z2) = (exp z2) * z1

now

let n be Element of NAT ; :: thesis: (z1 * (z2 rExpSeq )) . n = ((z2 rExpSeq ) * z1) . n
thus (z1 * (z2 rExpSeq )) . n = z1 * ((z2 rExpSeq ) . n) by LOPBAN_3:def 9
.= z1 * ((1 / (n ! )) * (z2 #N n)) by Def2
.= (1 / (n ! )) * (z1 * (z2 #N n)) by LOPBAN_3:43
.= (1 / (n ! )) * ((z2 #N n) * z1) by A1, Lm2
.= ((1 / (n ! )) * (z2 #N n)) * z1 by LOPBAN_3:43
.= ((z2 rExpSeq ) . n) * z1 by Def2
.= ((z2 rExpSeq ) * z1) . n by LOPBAN_3:def 10 ; :: thesis: verum

end;

then A2: z1 * (z2 rExpSeq ) = (z2 rExpSeq ) * z1 by FUNCT_2:113;
A3: Partial_Sums (z2 rExpSeq ) is convergent by LOPBAN_3:def 2;
thus z1 * (exp z2) = z1 * (Sum (z2 rExpSeq )) by Def10
.= lim (z1 * (Partial_Sums (z2 rExpSeq ))) by A3, Th6
.= lim (Partial_Sums (z1 * (z2 rExpSeq ))) by Th9
.= lim ((Partial_Sums (z2 rExpSeq )) * z1) by A2, Th9
.= (Sum (z2 rExpSeq )) * z1 by A3, Th7
.= (exp z2) * z1 by Def10 ; :: thesis: verum