let a, b be Complex; :: thesis: ( a * b = 1 implies a = b " )
assume A1: a * b = 1 ; :: thesis: a = b "
then b <> 0 ;
hence a = b " by A1, XCMPLX_0:def 7; :: thesis: verum