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

( (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