let a, b be Real; :: thesis: ( a >= 0 & b >= 0 implies a * (sqrt b) = sqrt ((a ^2) * b) )
assume that
A1: a >= 0 and
A2: b >= 0 ; :: thesis: a * (sqrt b) = sqrt ((a ^2) * b)
sqrt (a ^2) = a by A1, Def2;
hence a * (sqrt b) = sqrt ((a ^2) * b) by A1, A2, Th29; :: thesis: verum