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 A1: (abs x) * (abs y) = x * y by COMPLEX1:65;
( 0 <= abs x & 0 <= abs y ) by COMPLEX1:46;
hence sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y)) by A1, SQUARE_1:29; :: thesis: verum