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: 0 <= sqrt a by A1, Def2;

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

(sqrt (a * b)) ^2 = a * b by A1, A2, Def2

.= ((sqrt a) ^2) * b by A1, Def2

.= ((sqrt a) ^2) * ((sqrt b) ^2) by A2, Def2

.= ((sqrt a) * (sqrt b)) ^2 ;

hence sqrt (a * b) = sqrt (((sqrt a) * (sqrt b)) ^2) by A1, A2, Def2

.= (sqrt a) * (sqrt b) by A3, A4, Def2 ;

:: thesis: verum

assume that

A1: 0 <= a and

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

A3: 0 <= sqrt a by A1, Def2;

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

(sqrt (a * b)) ^2 = a * b by A1, A2, Def2

.= ((sqrt a) ^2) * b by A1, Def2

.= ((sqrt a) ^2) * ((sqrt b) ^2) by A2, Def2

.= ((sqrt a) * (sqrt b)) ^2 ;

hence sqrt (a * b) = sqrt (((sqrt a) * (sqrt b)) ^2) by A1, A2, Def2

.= (sqrt a) * (sqrt b) by A3, A4, Def2 ;

:: thesis: verum