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:95;
x = x #R ((1 / 2) * 2) by A1, PREPOWER:86
.= (x #R (1 / 2)) #R 2 by A1, PREPOWER:105
.= (x #R (1 / 2)) #Q 2 by A1, PREPOWER:88, PREPOWER:95
.= (x #R (1 / 2)) to_power 2 by A1, POWER:51, PREPOWER:95
.= (x #R (1 / 2)) ^2 by POWER:53 ;
hence x #R (1 / 2) = sqrt x by A1, A2, SQUARE_1:def 4; :: thesis: verum