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

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