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 abs (x * y) = x * y by Def1;
then ( (abs x) * (abs y) = x * y & 0 <= abs x & 0 <= abs y ) by COMPLEX1:132, COMPLEX1:151;
hence sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y)) by SQUARE_1:97; :: thesis: verum