let r be Real; :: thesis: Product (1 |-> r) = r
thus Product (1 |-> r) = Product <*r*> by FINSEQ_2:73
.= r by RVSUM_1:125 ; :: thesis: verum