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