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) by Def1;
then A1: x / y = (abs x) / (abs y) by COMPLEX1:67;
( 0 <= abs x & 0 <= abs y ) by COMPLEX1:46;
hence sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y)) by A1, SQUARE_1:30; :: thesis: verum