a |^ 2 = a ^2 by RING_5:3;
hence a |^ 2 is square ; :: thesis: verum