|.(a *').| = |.a.| by COMPLEX1:53;
hence a *' is weightless by Def3; :: thesis: verum