theorem :: SQUARE_1:33

for a being Real st 0 < a holds
(sqrt a) / a = 1 / (sqrt a)