|.(a |^ (2 * n)).| <= 1 by TA1;
hence not (a |^ (2 * n)) - 1 is positive ; :: thesis: verum