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

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