( |.a.| > 1 & |.b.| >= 1 ) by Def1, Def2;
then |.a.| * |.b.| > 1 * 1 by XREAL_1:97;
hence a * b is heavy by COMPLEX1:65; :: thesis: verum