:: deftheorem defines / XCMPLX_0:def 8 :
for x, y being Complex holds x / y = x * (y ");