let p, q be real number ; Sum ((p + q) rExpSeq ) = (Sum (p rExpSeq )) * (Sum (q rExpSeq ))
reconsider p = p, q = q as Real by XREAL_0:def 1;
A1: 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:29
.=
Re (((Re (Sum (p ExpSeq ))) + ((Im (Sum (p ExpSeq ))) * <i> )) * ((Re (Sum (q ExpSeq ))) + ((Im (Sum (q ExpSeq ))) * <i> )))
by COMPLEX1:29
.=
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:28
;
thus
Sum ((p + q) rExpSeq ) = (Sum (p rExpSeq )) * (Sum (q rExpSeq ))
by A1; verum