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