let x be Real; :: thesis: ( x > 0 implies x #R (1 / 2) = sqrt x )
assume A1: x > 0 ; :: thesis: x #R (1 / 2) = sqrt x
then A2: x #R (1 / 2) > 0 by PREPOWER:81;
x = x #R ((1 / 2) * 2) by A1, PREPOWER:72
.= (x #R (1 / 2)) #R 2 by A1, PREPOWER:91
.= (x #R (1 / 2)) #Q 2 by A1, PREPOWER:74, PREPOWER:81
.= (x #R (1 / 2)) to_power 2 by A1, POWER:44, PREPOWER:81
.= (x #R (1 / 2)) ^2 by POWER:46 ;
hence x #R (1 / 2) = sqrt x by A1, A2, SQUARE_1:def 2; :: thesis: verum