let th be Real; :: thesis: for th1 being real number st th = th1 holds
( |.(Sum ((th * <i>) ExpSeq)).| = 1 & abs (sin . th1) <= 1 & abs (cos . th1) <= 1 )
let th1 be real number ; :: thesis: ( th = th1 implies ( |.(Sum ((th * <i>) ExpSeq)).| = 1 & abs (sin . th1) <= 1 & abs (cos . th1) <= 1 ) )
assume A1: th = th1 ; :: thesis: ( |.(Sum ((th * <i>) ExpSeq)).| = 1 & abs (sin . th1) <= 1 & abs (cos . th1) <= 1 )
A2: (Sum ((th * <i>) ExpSeq)) * (Sum ((- (th * <i>)) ExpSeq)) = Sum (((th * <i>) + (- (th * <i>))) ExpSeq) by Lm2
.= 1r by Th10 ;
|.(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: ( abs (sin . th1) <= 1 & abs (cos . th1) <= 1 )
( abs (sin . th) = abs (Im (Sum ((th * <i>) ExpSeq))) & abs (cos . th) = abs (Re (Sum ((th * <i>) ExpSeq))) ) by Def20, Def22;
hence ( abs (sin . th1) <= 1 & abs (cos . th1) <= 1 ) by A1, A4, COMSEQ_3:13; :: thesis: verum