let p, q be Real; :: 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 Th45
.= (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