let a, b be real number ; :: thesis: ( 0 <= a & 0 <= b implies sqrt (a / b) = (sqrt a) / (sqrt b) )
assume A1: ( 0 <= a & 0 <= b ) ; :: thesis: sqrt (a / b) = (sqrt a) / (sqrt b)
then A2: ( 0 <= sqrt a & 0 <= sqrt b ) by Def4;
( ((sqrt a) / (sqrt b)) ^2 = ((sqrt a) ^2 ) / ((sqrt b) ^2 ) & (sqrt a) ^2 = a & (sqrt b) ^2 = b ) by A1, Def4, XCMPLX_1:77;
then ( 0 <= a / b & 0 <= (sqrt a) / (sqrt b) & ((sqrt a) / (sqrt b)) ^2 = a / b ) by A2;
hence sqrt (a / b) = (sqrt a) / (sqrt b) by Def4; :: thesis: verum