let a, b be Complex; :: thesis: ( a * (b ") = 1 implies a = b )
assume a * (b ") = 1 ; :: thesis: a = b
then a / b = 1 by XCMPLX_0:def 9;
hence a = b by Th58; :: thesis: verum