A1: |.a.| * |.(a *').| = |.(a * (a *')).| by COMPLEX1:65;
( a is weightless implies a *' is weightless ) ;
hence a * (a *') is weightless by A1, Def3; :: thesis: verum