reconsider b = |.a.| as positive Real ;
( not |.a.| <> 1 or |.a.| > 1 or |.a.| < 1 ) by XXREAL_0:1;
then ( |.a.| |^ n <> 1 * (0 |^ n) & |.a.| |^ n <> 1 |^ n ) by Def3, NEWTON02:40;
hence not a |^ n is weightless by TAYLOR21; :: thesis: verum