let th be real number ; :: thesis: ( ((cos . th) ^2 ) + ((sin . th) ^2 ) = 1 & ((cos . th) * (cos . th)) + ((sin . th) * (sin . th)) = 1 )
reconsider th1 = th as Real by XREAL_0:def 1;
A1: (Sum ((th1 * <i> ) ExpSeq )) * (Sum ((- (th1 * <i> )) ExpSeq )) = Sum (((th1 * <i> ) + (- (th1 * <i> ))) ExpSeq ) by Lm2
.= 1r by Th10 ;
thus ((cos . th) ^2 ) + ((sin . th) ^2 ) = ((Re (Sum ((th1 * <i> ) ExpSeq ))) ^2 ) + ((sin . th) ^2 ) by Def22
.= ((Re (Sum ((th1 * <i> ) ExpSeq ))) ^2 ) + ((Im (Sum ((th1 * <i> ) ExpSeq ))) ^2 ) by Def20
.= |.((Sum ((th1 * <i> ) ExpSeq )) * (Sum ((th1 * <i> ) ExpSeq ))).| by COMPLEX1:154
.= |.((Sum ((th1 * <i> ) ExpSeq )) * ((Sum ((th1 * <i> ) ExpSeq )) *' )).| by COMPLEX1:155
.= 1 by A1, Lm4, COMPLEX1:134 ; :: thesis: ((cos . th) * (cos . th)) + ((sin . th) * (sin . th)) = 1
hence ((cos . th) * (cos . th)) + ((sin . th) * (sin . th)) = 1 ; :: thesis: verum