let a, b be real number ; :: 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, Def4;
hence a * (sqrt b) = sqrt ((a ^2 ) * b) by A1, A2, Th97; :: thesis: verum