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