let a be positive Real; :: thesis: (sqrt a) / a = 1 / (sqrt a)
a = sqrt (a ^2) by SQUARE_1:def 2
.= (sqrt a) * (sqrt a) by SQUARE_1:29 ;
then (sqrt a) / a = ((sqrt a) / (sqrt a)) / (sqrt a) by XCMPLX_1:78;
hence (sqrt a) / a = 1 / (sqrt a) by XCMPLX_1:60, SQUARE_1:24; :: thesis: verum