let a be Real; :: thesis: ( 0 < a implies (sqrt a) / a = 1 / (sqrt a) )
assume A1: 0 < a ; :: thesis: (sqrt a) / a = 1 / (sqrt a)
then sqrt a <> 0 ^2 by Def2;
hence (sqrt a) / a = ((sqrt a) ^2) / (a * (sqrt a)) by XCMPLX_1:91
.= (1 * a) / ((sqrt a) * a) by A1, Def2
.= 1 / (sqrt a) by A1, XCMPLX_1:91 ;
:: thesis: verum