( |.a.| <= 1 & |.(a *').| <= 1 ) by Def1;
then |.a.| * |.(a *').| <= 1 * 1 by XREAL_1:66;
hence not a * (a *') is heavy by COMPLEX1:65; :: thesis: verum