let th be Real; :: thesis: ( ((cos . th) ^2) + ((sin . th) ^2) = 1 & ((cos . th) * (cos . th)) + ((sin . th) * (sin . th)) = 1 )
reconsider th1 = th as Real ;
A1: (Sum ((th1 * <i>) ExpSeq)) * (Sum ((- (th1 * <i>)) ExpSeq)) = Sum (((th1 * <i>) + (- (th1 * <i>))) ExpSeq) by Lm2
.= 1r by Th9 ;
thus ((cos . th) ^2) + ((sin . th) ^2) = ((Re (Sum ((th1 * <i>) ExpSeq))) ^2) + ((sin . th) ^2) by Def18
.= ((Re (Sum ((th1 * <i>) ExpSeq))) ^2) + ((Im (Sum ((th1 * <i>) ExpSeq))) ^2) by Def16
.= |.((Sum ((th1 * <i>) ExpSeq)) * (Sum ((th1 * <i>) ExpSeq))).| by COMPLEX1:68
.= |.((Sum ((th1 * <i>) ExpSeq)) * ((Sum ((th1 * <i>) ExpSeq)) *')).| by COMPLEX1:69
.= 1 by A1, Lm4, COMPLEX1:48 ; :: thesis: ((cos . th) * (cos . th)) + ((sin . th) * (sin . th)) = 1
hence ((cos . th) * (cos . th)) + ((sin . th) * (sin . th)) = 1 ; :: thesis: verum