theorem :: ABSVALUE:8

for x, y being Real st 0 <= x * y holds
sqrt (x * y) = (sqrt |.x.|) * (sqrt |.y.|)