let z, z1, z2 be Complex; :: thesis: for X being complex-membered set holds
( [z1,z2] in multRel (X,z) iff ( z1 in X & z2 in X & z2 = z * z1 ) )
let X be complex-membered set ; :: thesis: ( [z1,z2] in multRel (X,z) iff ( z1 in X & z2 in X & z2 = z * z1 ) )
reconsider g = (curry multcomplex) . z as Function ;
( z in COMPLEX & z1 in COMPLEX ) by XCMPLX_0:def 2;
then [z,z1] in [:COMPLEX,COMPLEX:] by ZFMISC_1:87;
then A1: [z,z1] in dom multcomplex by FUNCT_2:def 1;

hereby :: thesis: ( z1 in X & z2 in X & z2 = z * z1 implies [z1,z2] in multRel (X,z) )

assume [z1,z2] in multRel (X,z) ; :: thesis: ( z1 in X & z2 in X & z2 = z * z1 )
then ( [z1,z2] in g |_2 X & z1 is set & z2 is set ) by TARSKI:1;
then A2: ( z1 in X & z2 in X & [z1,z2] in g ) by MMLQUER2:4;
then ( z1 in dom g & g . z1 = z2 ) by FUNCT_1:1;
then z2 = multcomplex . (z,z1) by A1, FUNCT_5:20;
hence ( z1 in X & z2 in X & z2 = z * z1 ) by A2, BINOP_2:def 5; :: thesis: verum

end;

assume A3: ( z1 in X & z2 in X & z2 = z * z1 ) ; :: thesis: [z1,z2] in multRel (X,z)
then A4: z2 = multcomplex . (z,z1) by BINOP_2:def 5
.= g . z1 by A1, FUNCT_5:20 ;
z1 in dom g by A1, FUNCT_5:20;
hence [z1,z2] in multRel (X,z) by A3, A4, FUNCT_1:1, MMLQUER2:4; :: thesis: verum