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