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 ;
A3: |.(Sum ((th * <i> ) ExpSeq )).| * |.(Sum ((th * <i> ) ExpSeq )).| = |.((Sum ((th * <i> ) ExpSeq )) * (Sum ((th * <i> ) ExpSeq ))).| by COMPLEX1:151
.= |.((Sum ((th * <i> ) ExpSeq )) * ((Sum ((th * <i> ) ExpSeq )) *' )).| by COMPLEX1:155
.= 1 by A2, Lm4, COMPLEX1:134 ;
thus A4: |.(Sum ((th * <i> ) ExpSeq )).| = 1 :: thesis: ( abs (sin . th1) <= 1 & abs (cos . th1) <= 1 )

proof

A5: |.(Sum ((th * <i> ) ExpSeq )).| = 1 / |.(Sum ((th * <i> ) ExpSeq )).| by A3, XCMPLX_1:74;
A6: |.(Sum ((th * <i> ) ExpSeq )).| <> 0 by A3;
|.(Sum ((th * <i> ) ExpSeq )).| <> - 1 by COMPLEX1:132;
hence |.(Sum ((th * <i> ) ExpSeq )).| = 1 by A5, A6, XCMPLX_1:200; :: thesis: verum

end;

A7: abs (sin . th) = abs (Im (Sum ((th * <i> ) ExpSeq ))) by Def20;
abs (cos . th) = abs (Re (Sum ((th * <i> ) ExpSeq ))) by Def22;
hence ( abs (sin . th1) <= 1 & abs (cos . th1) <= 1 ) by A1, A4, A7, COMSEQ_3:13; :: thesis: verum