reconsider k = |.a.| as Element of NAT by INT_1:3;
k |^ n = |.(a |^ n).| by TAYLOR_2:1;
hence a |^ n is square ; :: thesis: verum