let p, q be Real; :: thesis: Sum ((p + q) rExpSeq) = (Sum (p rExpSeq)) * (Sum (q rExpSeq))
reconsider p = p, q = q as Real ;
Sum ((p + q) rExpSeq) = Re (Sum ((p + q) ExpSeq)) by Th44
.= 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 Th44
.= Re (((Sum (p rExpSeq)) + (0 * <i>)) * ((Re (Sum (q ExpSeq))) + ((Im (Sum (q ExpSeq))) * <i>))) by Th41
.= Re ((Sum (p rExpSeq)) * ((Sum (q rExpSeq)) + ((Im (Sum (q ExpSeq))) * <i>))) by Th44
.= Re ((Sum (p rExpSeq)) * ((Sum (q rExpSeq)) + (0 * <i>))) by Th41
.= 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