let p, q be real number ; :: thesis: exp_R . (p + q) = (exp_R . p) * (exp_R . q)
A1: 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 ;
thus exp_R . (p + q) = (exp_R . p) * (exp_R . q) by A1; :: thesis: verum