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 <= a * b ;
then A3: (sqrt (a * b)) ^2 = a * b by Def4
.= ((sqrt a) ^2 ) * b by A1, Def4
.= ((sqrt a) ^2 ) * ((sqrt b) ^2 ) by A1, Def4
.= ((sqrt a) * (sqrt b)) ^2 ;
( 0 <= sqrt a & 0 <= sqrt b ) by A1, Def4;
then A4: ( 0 <= sqrt (a * b) & 0 <= (sqrt a) * (sqrt b) ) by A2, Def4;
thus sqrt (a * b) = sqrt (((sqrt a) * (sqrt b)) ^2 ) by A2, A3, Def4
.= (sqrt a) * (sqrt b) by A4, Lm3 ; :: thesis: verum