theorem Th29: :: SQUARE_1:29

for a, b being Real st 0 <= a & 0 <= b holds
sqrt (a * b) = (sqrt a) * (sqrt b)