theorem :: NUMBER17:89

for a being positive Real holds 2 -root a = sqrt a