( a is heavy implies a *' is heavy ) ;
then |.a.| * |.(a *').| > 1 * 1 by Def1, XREAL_1:97;
hence a * (a *') is heavy by COMPLEX1:65; :: thesis: verum