for th being Real holds
( |.(exp (th * <i>)).| = 1 & ( for th being Real holds
( |.(sin th).| <= 1 & |.(cos th).| <= 1 ) ) )