let x be real number ; :: thesis: ( x >= 0 implies sqrt x = x to_power (1 / 2) )
assume A1: x >= 0 ; :: thesis: sqrt x = x to_power (1 / 2)

per cases ( x = 0 or x > 0 ) by A1;

suppose x = 0 ; :: thesis: sqrt x = x to_power (1 / 2)

hence sqrt x = x to_power (1 / 2) by POWER:def 2, SQUARE_1:82; :: thesis: verum

end;

suppose A2: x > 0 ; :: thesis: sqrt x = x to_power (1 / 2)

then A3: x to_power (1 / 2) > 0 by POWER:39;
(x to_power (1 / 2)) ^2 = (x to_power (1 / 2)) to_power 2 by POWER:53
.= x to_power ((1 / 2) * 2) by A2, POWER:38
.= x by POWER:30 ;
hence sqrt x = x to_power (1 / 2) by A3, SQUARE_1:89; :: thesis: verum

end;

end;