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

suppose |.a.| = 0 ; :: thesis: a |^ n is weightless

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

end;

suppose |.a.| = 1 ; :: thesis: a |^ n is weightless

then 1 = |.a.| |^ n
.= |.(a |^ n).| by TAYLOR21 ;
hence a |^ n is weightless ; :: thesis: verum

end;

end;