1 * (1 ") = 1 " by Th3;
hence 1 " = 1 by XCMPLX_0:def 7; :: thesis: verum