reconsider x = b / 2 as Nat ;
reconsider k = a |^ x as Element of NAT by ORDINAL1:def 12;
a |^ (2 * x) = (a |^ x) |^ 2 by NEWTON:9;
hence a |^ b is square ; :: thesis: verum