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