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