theorem :: TOPREAL6:6

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