let r be Real; :: thesis: Product (2 |-> r) = r * r
thus Product (2 |-> r) = Product <*r,r*> by FINSEQ_2:75
.= r * r by RVSUM_1:129 ; :: thesis: verum