let a be real number ; :: 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 Def4;
hence (sqrt a) / a = ((sqrt a) ^2 ) / (a * (sqrt a)) by XCMPLX_1:92
.= (1 * a) / ((sqrt a) * a) by A1, Def4
.= 1 / (sqrt a) by A1, XCMPLX_1:92 ;
:: thesis: verum