a |^ 2 = a ^2 by NEWTON:81;
hence sqrt (a |^ 2) = a by SQUARE_1:22; :: thesis: verum