theorem Th54: :: SQUARE_1:54

for a, b being Real st a >= 0 & b >= 0 holds
a * (sqrt b) = sqrt ((a ^2) * b)