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