let X be Complex_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 * ((- 1r ) * z) by CLOPBAN3:42
.= (- 1r ) * (z * z) by CLOPBAN3:42
.= ((- 1r ) * z) * z by CLOPBAN3:42
.= (- z) * z by CLOPBAN3:42 ;
then A1: z, - z are_commutative by LOPBAN_4:def 1;
hence (exp z) * (exp (- z)) = exp (z + (- z)) by Th34
.= exp (0. X) by RLVECT_1:16
.= 1. X by Th36 ;
:: thesis: (exp (- z)) * (exp z) = 1. X
thus (exp (- z)) * (exp z) = exp ((- z) + z) by A1, Th34
.= exp (0. X) by RLVECT_1:16
.= 1. X by Th36 ; :: thesis: verum