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 ;
A4: ( |.(Sum ((th * <i> ) ExpSeq )).| = 1 / |.(Sum ((th * <i> ) ExpSeq )).| & |.(Sum ((th * <i> ) ExpSeq )).| <> 0 ) by A3, XCMPLX_1:74;
A5: |.(Sum ((th * <i> ) ExpSeq )).| <> - 1 by COMPLEX1:132;
thus A6: |.(Sum ((th * <i> ) ExpSeq )).| = 1 by A4, A5, XCMPLX_1:200; :: thesis: ( abs (sin . th1) <= 1 & abs (cos . th1) <= 1 )
A7: ( abs (sin . th) = abs (Im (Sum ((th * <i> ) ExpSeq ))) & abs (cos . th) = abs (Re (Sum ((th * <i> ) ExpSeq ))) ) by Def20, Def22;
thus ( abs (sin . th1) <= 1 & abs (cos . th1) <= 1 ) by A1, A6, A7, COMSEQ_3:13; :: thesis: verum