( 0 <= |.a.| & |.a.| < 1 & 0 <= |.b.| & |.b.| <= 1 ) by Def1, Def2;
then |.a.| * |.b.| < 1 by XREAL_1:162;
hence a * b is light by COMPLEX1:65; :: thesis: verum