let th be Real; :: thesis: ( cos . 0 = 1 & sin . 0 = 0 & cos . (- th) = cos . th & sin . (- th) = - (sin . th) )
thus cos . 0 = Re (Sum ((0 * <i>) ExpSeq)) by Def18
.= 1 by Th9, COMPLEX1:6 ; :: thesis: ( sin . 0 = 0 & cos . (- th) = cos . th & sin . (- th) = - (sin . th) )
thus sin . 0 = Im (Sum ((0 * <i>) ExpSeq)) by Def16
.= 0 by Th9, COMPLEX1:6 ; :: thesis: ( cos . (- th) = cos . th & sin . (- th) = - (sin . th) )
reconsider th1 = th as Real ;
thus cos . (- th) = Re (Sum (((- 0) + ((- th1) * <i>)) ExpSeq)) by Def18
.= Re (Sum ((- (th1 * <i>)) ExpSeq))
.= Re ((Sum ((th1 * <i>) ExpSeq)) *') by Lm4
.= Re (((cos . th) + ((sin . th) * <i>)) *') by Lm3
.= Re ((cos . th) + ((- (sin . th)) * <i>)) by Lm1
.= cos . th by COMPLEX1:12 ; :: thesis: sin . (- th) = - (sin . th)
thus sin . (- th) = Im (Sum (((- 0) + ((- th1) * <i>)) ExpSeq)) by Def16
.= Im (Sum ((- (th1 * <i>)) ExpSeq))
.= Im ((Sum ((th1 * <i>) ExpSeq)) *') by Lm4
.= Im (((cos . th) + ((sin . th) * <i>)) *') by Lm3
.= Im ((cos . th) + ((- (sin . th)) * <i>)) by Lm1
.= - (sin . th) by COMPLEX1:12 ; :: thesis: verum