theorem Th4: :: TOPREAL6:5

for rr being Real holds Product (1 |-> rr) = rr