let th, th1 be Real; :: thesis: ( th = th1 implies ( |.(Sum ((th * <i>) ExpSeq)).| = 1 & |.(sin . th1).| <= 1 & |.(cos . th1).| <= 1 ) )
assume A1: th = th1 ; :: thesis: ( |.(Sum ((th * <i>) ExpSeq)).| = 1 & |.(sin . th1).| <= 1 & |.(cos . th1).| <= 1 )
A2: (Sum ((th * <i>) ExpSeq)) * (Sum ((- (th * <i>)) ExpSeq)) = Sum (((th * <i>) + (- (th * <i>))) ExpSeq) by Lm2
.= 1r by Th9 ;
|.(Sum ((th * <i>) ExpSeq)).| * |.(Sum ((th * <i>) ExpSeq)).| = |.((Sum ((th * <i>) ExpSeq)) * (Sum ((th * <i>) ExpSeq))).| by COMPLEX1:65
.= |.((Sum ((th * <i>) ExpSeq)) * ((Sum ((th * <i>) ExpSeq)) *')).| by COMPLEX1:69
.= 1 by A2, Lm4, COMPLEX1:48 ;
then A3: ( |.(Sum ((th * <i>) ExpSeq)).| = 1 / |.(Sum ((th * <i>) ExpSeq)).| & |.(Sum ((th * <i>) ExpSeq)).| <> 0 ) by XCMPLX_1:73;
|.(Sum ((th * <i>) ExpSeq)).| <> - 1 by COMPLEX1:46;
hence A4: |.(Sum ((th * <i>) ExpSeq)).| = 1 by A3, XCMPLX_1:199; :: thesis: ( |.(sin . th1).| <= 1 & |.(cos . th1).| <= 1 )
( |.(sin . th).| = |.(Im (Sum ((th * <i>) ExpSeq))).| & |.(cos . th).| = |.(Re (Sum ((th * <i>) ExpSeq))).| ) by Def16, Def18;
hence ( |.(sin . th1).| <= 1 & |.(cos . th1).| <= 1 ) by A1, A4, COMSEQ_3:13; :: thesis: verum