let x, y be Real; :: thesis: ( 0 < x / y implies sqrt (x / y) = (sqrt |.x.|) / (sqrt |.y.|) )
assume 0 < x / y ; :: thesis: sqrt (x / y) = (sqrt |.x.|) / (sqrt |.y.|)
then x / y = |.(x / y).| by Def1;
then A1: x / y = |.x.| / |.y.| by COMPLEX1:67;
( 0 <= |.x.| & 0 <= |.y.| ) by COMPLEX1:46;
hence sqrt (x / y) = (sqrt |.x.|) / (sqrt |.y.|) by A1, SQUARE_1:30; :: thesis: verum