theorem :: BKMODEL3:10

for a being positive Real holds (sqrt a) / a = 1 / (sqrt a)