theorem :: SIN_COS:25

for th being Real holds exp (th * <i>) = (cos th) + ((sin th) * <i>)