let a be non negative Real; :: thesis: (sqrt a) * (sqrt a) = a

a = sqrt (a ^2) by SQUARE_1:22

.= (sqrt a) * (sqrt a) by SQUARE_1:29 ;

hence (sqrt a) * (sqrt a) = a ; :: thesis: verum

a = sqrt (a ^2) by SQUARE_1:22

.= (sqrt a) * (sqrt a) by SQUARE_1:29 ;

hence (sqrt a) * (sqrt a) = a ; :: thesis: verum