let th1, th2 be Real; :: 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 ;
A1: (th1 + th2) * <i> = (0 + 0) + ((th1 + th2) * <i>) ;
A2: (Sum ((th1 * <i>) ExpSeq)) * (Sum ((th2 * <i>) ExpSeq)) = Sum (((th1 * <i>) + (th2 * <i>)) ExpSeq) by Lm2
.= (cos . (th1 + th2)) + ((sin . (th1 + th2)) * <i>) by A1, 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 A2, COMPLEX1:77; :: thesis: verum