let p, q be real number ; :: thesis: exp_R . (p + q) = (exp_R . p) * (exp_R . q)
exp_R . (p + q) = Sum ((p + q) rExpSeq) by Def26
.= (Sum (p rExpSeq)) * (Sum (q rExpSeq)) by Th50
.= (exp_R . p) * (Sum (q rExpSeq)) by Def26
.= (exp_R . p) * (exp_R . q) by Def26 ;
hence exp_R . (p + q) = (exp_R . p) * (exp_R . q) ; :: thesis: verum