:: deftheorem Def6 defines " XCMPLX_0:def 6 :
for z, b₂ being Complex holds
( ( z <> 0 implies ( b₂ = z " iff z * b₂ = 1 ) ) & ( not z <> 0 implies ( b₂ = z " iff b₂ = 0 ) ) );