let x be Complex; :: thesis: 0 / x = 0
0 / x = 0 * (x ") by XCMPLX_0:def 9;
hence 0 / x = 0 by Th2; :: thesis: verum