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

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