let th be Real; :: thesis: ( |.(exp (th * <i>)).| = 1 & ( for th being Real holds
( |.(sin th).| <= 1 & |.(cos th).| <= 1 ) ) )
thus |.(exp (th * <i>)).| = |.(Sum ((th * <i>) ExpSeq)).| by Def14
.= 1 by Lm5 ; :: thesis: for th being Real holds
( |.(sin th).| <= 1 & |.(cos th).| <= 1 )
let th be Real; :: thesis: ( |.(sin th).| <= 1 & |.(cos th).| <= 1 )
thus |.(sin th).| <= 1 by Lm5; :: thesis: |.(cos th).| <= 1
thus |.(cos th).| <= 1 by Lm5; :: thesis: verum