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