theorem :: SQUARE_1:32

for a being Real st 0 < a holds
sqrt (1 / a) = 1 / (sqrt a) by Th18, Th30;