let p, q be Real; :: thesis: exp_R . (p + q) = (exp_R . p) * (exp_R . q)
exp_R . (p + q) = exp_R (p + q) by SIN_COS:def 23
.= (exp_R p) * (exp_R q) by SIN_COS:50
.= (exp_R . p) * (exp_R q) by SIN_COS:def 23
.= (exp_R . p) * (exp_R . q) by SIN_COS:def 23 ;
hence exp_R . (p + q) = (exp_R . p) * (exp_R . q) ; :: thesis: verum