theorem :: SQUARE_1:34

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