( |.a.| < 1 & |.(a *').| < 1 ) by Def2;
then |.a.| * |.(a *').| < 1 * 1 by XREAL_1:96;
hence a * (a *') is light by COMPLEX1:65; :: thesis: verum