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