:: deftheorem defines exp CLOPBAN4:def 7 :
for X being Complex_Banach_Algebra
for z being Element of X holds exp z = (exp_ X) . z;