for X being Complex_Banach_Algebra
for z being Element of X holds
( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X )