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