theorem :: ABSVALUE:10

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