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