consider k being Nat such that
A1: k ^2 = a by PYTHTRIP:def 3;
a |^ n = k |^ (2 * n) by A1, NEWTON:9
.= (k |^ n) ^2 by NEWTON:9 ;
hence a |^ n is square ; :: thesis: verum