let a, b be real number ; :: thesis: ( a >= 0 & b >= 0 implies a * (sqrt b) = sqrt ((a ^2 ) * b) )
assume A1: ( a >= 0 & b >= 0 ) ; :: thesis: a * (sqrt b) = sqrt ((a ^2 ) * b)
then A2: sqrt (a ^2 ) = a by Lm3;
thus a * (sqrt b) = sqrt ((a ^2 ) * b) by A1, A2, Th97; :: thesis: verum