per cases ( |.a.| = 1 or |.a.| = 0 ) by Def3;
suppose |.a.| = 1 ; :: thesis: a * b is weightless
then |.(a * b).| = |.1.| * |.b.| by COMPLEX1:65
.= |.b.| ;
hence a * b is weightless by Def3; :: thesis: verum
end;
suppose |.a.| = 0 ; :: thesis: a * b is weightless
then |.(a * b).| = |.0.| * |.b.| by COMPLEX1:65
.= 0 ;
hence a * b is weightless ; :: thesis: verum
end;
end;