let x be Real; :: 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; :: 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:34;
(x to_power (1 / 2)) ^2 = (x to_power (1 / 2)) to_power 2 by POWER:46
.= x to_power ((1 / 2) * 2) by A2, POWER:33
.= x by POWER:25 ;
hence sqrt x = x to_power (1 / 2) by A3, SQUARE_1:22; :: thesis: verum

end;

end;