:: deftheorem defines exp SIN_COS:def 15 :
for z being Complex holds exp z = exp . z;