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 CLVECT_1:3
.= (- 1r) * (z * z) by CLOPBAN3:38
.= ((- 1r) * z) * z by CLOPBAN3:38
.= (- z) * z by CLVECT_1:3 ;
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:5
.= 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:5
.= 1. X by Th36 ; :: thesis: verum