:: deftheorem defines exp LOPBAN_4:def 11 :
for X being Banach_Algebra
for z being Element of X holds exp z = (exp_ X) . z;