b * (b ") = b / b
.= 1 by XCMPLX_1:60 ;
hence ( b * (b ") is weightless & b * (b ") is positive ) ; :: thesis: verum