A0: 2 = |.2.| ;
A2: ( k > 0 & |.u.| is even implies |.u.| |^ k is even ) by PEPIN:21;
|.(u |^ k).| = |.u.| |^ k by TAYLOR_2:1;
hence u |^ k is even by A2, A0, ABIAN:def 1, INT_2:16; :: thesis: verum