let th1, th2 be real number ; :: thesis: ( sin . (th1 + th2) = ((sin . th1) * (cos . th2)) + ((cos . th1) * (sin . th2)) & cos . (th1 + th2) = ((cos . th1) * (cos . th2)) - ((sin . th1) * (sin . th2)) )
reconsider th1 = th1, th2 = th2 as Real by XREAL_0:def 1;
A2: (th1 + th2) * <i> = (0 + 0 ) + ((th1 + th2) * <i> ) ;
A4: (Sum ((th1 * <i> ) ExpSeq )) * (Sum ((th2 * <i> ) ExpSeq )) = Sum (((th1 * <i> ) + (th2 * <i> )) ExpSeq ) by Lm2
.= (cos . (th1 + th2)) + ((sin . (th1 + th2)) * <i> ) by A2, Lm3 ;
(Sum ((th1 * <i> ) ExpSeq )) * (Sum ((th2 * <i> ) ExpSeq )) = ((cos . th1) + ((sin . th1) * <i> )) * (Sum ((th2 * <i> ) ExpSeq )) by Lm3
.= ((cos . th1) + ((sin . th1) * <i> )) * ((cos . th2) + ((sin . th2) * <i> )) by Lm3
.= (((cos . th1) * (cos . th2)) - ((sin . th1) * (sin . th2))) + ((((sin . th1) * (cos . th2)) + ((cos . th1) * (sin . th2))) * <i> ) ;
hence ( sin . (th1 + th2) = ((sin . th1) * (cos . th2)) + ((cos . th1) * (sin . th2)) & cos . (th1 + th2) = ((cos . th1) * (cos . th2)) - ((sin . th1) * (sin . th2)) ) by A4, COMPLEX1:163; :: thesis: verum