per cases ( a is zero or not a is zero ) ;

suppose a is zero ; :: thesis: a / |.a.| is weightless

hence a / |.a.| is weightless ; :: thesis: verum

end;

suppose not a is zero ; :: thesis: a / |.a.| is weightless

then reconsider b = |.a.| as non zero Real ;
1 = (1 * b) / |.b.| by XCMPLX_1:89
.= |.(a / |.a.|).| by COMPLEX1:67 ;
hence a / |.a.| is weightless ; :: thesis: verum

end;

end;