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;