reconsider a = a as square Element of NAT by ORDINAL1:def 12;
a |^ n is square ;
hence a |^ n is square ; :: thesis: verum