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 Def22
.= (Sum (p rExpSeq)) * (Sum (q rExpSeq)) by Th46
.= (exp_R . p) * (Sum (q rExpSeq)) by Def22
.= (exp_R . p) * (exp_R . q) by Def22 ;
hence exp_R . (p + q) = (exp_R . p) * (exp_R . q) ; :: thesis: verum