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 5
.= z1 * ((1 / (n !)) * (z2 #N n)) by Def2
.= (1 / (n !)) * (z1 * (z2 #N n)) by LOPBAN_3:38
.= (1 / (n !)) * ((z2 #N n) * z1) by A1, Lm2
.= ((1 / (n !)) * (z2 #N n)) * z1 by LOPBAN_3:38
.= ((z2 rExpSeq) . n) * z1 by Def2
.= ((z2 rExpSeq) * z1) . n by LOPBAN_3:def 6 ; :: thesis: verum

end;

then A2: z1 * (z2 rExpSeq) = (z2 rExpSeq) * z1 by FUNCT_2:63;
A3: Partial_Sums (z2 rExpSeq) is convergent by LOPBAN_3:def 1;
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