let x, y be real number ; :: thesis: ( 0 < x / y implies sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y)) )
assume 0 < x / y ; :: thesis: sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y))
then ( x / y = abs (x / y) & 0 <= abs y ) by Def1, COMPLEX1:132;
then ( x / y = (abs x) / (abs y) & 0 <= abs x & 0 <= abs y ) by COMPLEX1:132, COMPLEX1:153;
hence sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y)) by SQUARE_1:99; :: thesis: verum