let th be Real; :: thesis: ( |.(exp (th * <i> )).| = 1 & ( for th being real number holds
( abs (sin th) <= 1 & abs (cos th) <= 1 ) ) )
thus |.(exp (th * <i> )).| = |.(Sum ((th * <i> ) ExpSeq )).| by Def18
.= 1 by Lm5 ; :: thesis: for th being real number holds
( abs (sin th) <= 1 & abs (cos th) <= 1 )
let th be real number ; :: thesis: ( abs (sin th) <= 1 & abs (cos th) <= 1 )
A1: th is Real by XREAL_0:def 1;
thus abs (sin th) <= 1 by A1, Lm5; :: thesis: abs (cos th) <= 1
thus abs (cos th) <= 1 by A1, Lm5; :: thesis: verum