let p, q be real number ; :: thesis: exp_R . (p + q) = (exp_R . p) * (exp_R . q)
exp_R . (p + q) = exp_R (p + q) by SIN_COS:def 27
.= (exp_R p) * (exp_R q) by SIN_COS:55
.= (exp_R . p) * (exp_R q) by SIN_COS:def 27
.= (exp_R . p) * (exp_R . q) by SIN_COS:def 27 ;
hence exp_R . (p + q) = (exp_R . p) * (exp_R . q) ; :: thesis: verum