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

suppose a = 0 ; :: thesis: a " is weightless

hence a " is weightless ; :: thesis: verum

end;

suppose |.a.| = 1 ; :: thesis: a " is weightless

then |.(a ").| = 1 " by COMPLEX1:66;
hence a " is weightless ; :: thesis: verum

end;

end;