let rr be Real; :: thesis: Product (2 |-> rr) = rr * rr
thus Product (2 |-> rr) = Product <*rr,rr*> by FINSEQ_2:61
.= rr * rr by RVSUM_1:99 ; :: thesis: verum