( |.a.| >= 1 & |.(a *').| >= 1 ) by Def2;
then |.a.| * |.(a *').| >= 1 * 1 by XREAL_1:66;
hence not a * (a *') is light by COMPLEX1:65; :: thesis: verum