let p, q be real number ; :: thesis: Sum ((p + q) rExpSeq) = (Sum (p rExpSeq)) * (Sum (q rExpSeq))
reconsider p = p, q = q as Real by XREAL_0:def 1;
Sum ((p + q) rExpSeq) = Re (Sum ((p + q) ExpSeq)) by Th49
.= Re ((Sum (p ExpSeq)) * (Sum (q ExpSeq))) by Lm2
.= Re (((Re (Sum (p ExpSeq))) + ((Im (Sum (p ExpSeq))) * <i>)) * (Sum (q ExpSeq))) by COMPLEX1:13
.= Re (((Re (Sum (p ExpSeq))) + ((Im (Sum (p ExpSeq))) * <i>)) * ((Re (Sum (q ExpSeq))) + ((Im (Sum (q ExpSeq))) * <i>))) by COMPLEX1:13
.= Re (((Sum (p rExpSeq)) + ((Im (Sum (p ExpSeq))) * <i>)) * ((Re (Sum (q ExpSeq))) + ((Im (Sum (q ExpSeq))) * <i>))) by Th49
.= Re (((Sum (p rExpSeq)) + (0 * <i>)) * ((Re (Sum (q ExpSeq))) + ((Im (Sum (q ExpSeq))) * <i>))) by Th46
.= Re ((Sum (p rExpSeq)) * ((Sum (q rExpSeq)) + ((Im (Sum (q ExpSeq))) * <i>))) by Th49
.= Re ((Sum (p rExpSeq)) * ((Sum (q rExpSeq)) + (0 * <i>))) by Th46
.= Re (((Sum (p rExpSeq)) * (Sum (q rExpSeq))) + (0 * <i>))
.= (Sum (p rExpSeq)) * (Sum (q rExpSeq)) by COMPLEX1:12 ;
hence Sum ((p + q) rExpSeq) = (Sum (p rExpSeq)) * (Sum (q rExpSeq)) ; :: thesis: verum