let X be Banach_Algebra; :: thesis: for z being Element of X holds
( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X )
let z be Element of X; :: thesis: ( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X )
z * (- z) = z * ((- 1) * z) by LOPBAN_3:38
.= (- 1) * (z * z) by LOPBAN_3:38
.= ((- 1) * z) * z by LOPBAN_3:38
.= (- z) * z by LOPBAN_3:38 ;
then A1: z, - z are_commutative by Def1;
hence (exp z) * (exp (- z)) = exp (z + (- z)) by Th35
.= exp (0. X) by RLVECT_1:5
.= 1. X by Th37 ;
:: thesis: (exp (- z)) * (exp z) = 1. X
thus (exp (- z)) * (exp z) = exp ((- z) + z) by A1, Th35
.= exp (0. X) by RLVECT_1:5
.= 1. X by Th37 ; :: thesis: verum