theorem Th7: :: XCMPLX_1:7

for a, b being Complex st b <> 0 & a * b = b holds
a = 1