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