theorem Th30: :: SQUARE_1:30

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