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