let a be non negative real number ; :: thesis: (sqrt a) * (sqrt a) = a
a = sqrt (a ^2 ) by SQUARE_1:89
.= (sqrt a) * (sqrt a) by SQUARE_1:97 ;
hence (sqrt a) * (sqrt a) = a ; :: thesis: verum