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