per cases ( |.a.| = 0 or |.a.| = 1 ) by Def3;

suppose |.a.| = 0 ; :: thesis: (a |^ (2 * n)) - 1 is weightless

then a = 0 ;
then ( a |^ (2 * n) = 0 or n = 0 ) by NAT_1:14, NEWTON:11;
then ( a |^ (2 * n) = 0 or a |^ (2 * n) = 1 ) by NEWTON:4;
hence (a |^ (2 * n)) - 1 is weightless ; :: thesis: verum

end;

suppose |.a.| = 1 ; :: thesis: (a |^ (2 * n)) - 1 is weightless

then ( a = 1 or - a = 1 ) by ABSVALUE:1;
hence (a |^ (2 * n)) - 1 is weightless ; :: thesis: verum

end;

end;