let x be Complex; :: thesis: x / 1 = x
x / 1 = x * 1 by Lm3, XCMPLX_0:def 9;
hence x / 1 = x by Th3; :: thesis: verum