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;