let z, z1 be Complex; :: thesis: [z1,(z1 * z)] in multRel (COMPLEX,z)
( z1 in COMPLEX & z1 * z in COMPLEX ) by XCMPLX_0:def 2;
hence [z1,(z1 * z)] in multRel (COMPLEX,z) by Th42; :: thesis: verum