theorem :: ASYMPT_1:83

for c being Real st c >= 0 holds
c to_power (1 / 2) = sqrt c by Lm39;