let a, b be Real; :: thesis: ( 0 <= a & 0 <= b implies sqrt (a / b) = (sqrt a) / (sqrt b) )

assume that

A1: 0 <= a and

A2: 0 <= b ; :: thesis: sqrt (a / b) = (sqrt a) / (sqrt b)

A3: (sqrt b) ^2 = b by A2, Def2;

(sqrt a) ^2 = a by A1, Def2;

then A4: ((sqrt a) / (sqrt b)) ^2 = a / b by A3, XCMPLX_1:76;

A5: 0 <= sqrt b by A2, Def2;

0 <= sqrt a by A1, Def2;

hence sqrt (a / b) = (sqrt a) / (sqrt b) by A5, A4, Def2; :: thesis: verum

assume that

A1: 0 <= a and

A2: 0 <= b ; :: thesis: sqrt (a / b) = (sqrt a) / (sqrt b)

A3: (sqrt b) ^2 = b by A2, Def2;

(sqrt a) ^2 = a by A1, Def2;

then A4: ((sqrt a) / (sqrt b)) ^2 = a / b by A3, XCMPLX_1:76;

A5: 0 <= sqrt b by A2, Def2;

0 <= sqrt a by A1, Def2;

hence sqrt (a / b) = (sqrt a) / (sqrt b) by A5, A4, Def2; :: thesis: verum