let z1, z2 be Complex; :: thesis: (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2)) = multRel (COMPLEX,(z1 * z2))
A1: (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2)) c= multRel (COMPLEX,(z1 * z2)) by Th51;

now :: thesis: for x, y being object st [x,y] in multRel (COMPLEX,(z1 * z2)) holds
[x,y] in (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2))

let x, y be object ; :: thesis: ( [x,y] in multRel (COMPLEX,(z1 * z2)) implies [x,y] in (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2)) )
reconsider a = x, b = y as set by TARSKI:1;
assume A2: [x,y] in multRel (COMPLEX,(z1 * z2)) ; :: thesis: [x,y] in (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2))
then [a,b] in multRel (COMPLEX,(z1 * z2)) ;
then A3: ( a in COMPLEX & b in COMPLEX ) by MMLQUER2:4;
then reconsider a = a, b = b as Complex ;
A4: b = (z1 * z2) * a by A2, Th42;
set c = z1 * a;
( z1 * a in COMPLEX & b = z2 * (z1 * a) ) by A4, XCMPLX_0:def 2;
then ( [a,(z1 * a)] in multRel (COMPLEX,z1) & [(z1 * a),b] in multRel (COMPLEX,z2) ) by A3, Th42;
hence [x,y] in (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2)) by RELAT_1:def 8; :: thesis: verum

end;

then multRel (COMPLEX,(z1 * z2)) c= (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2)) by RELAT_1:def 3;
hence (multRel (COMPLEX,z1)) * (multRel (COMPLEX,z2)) = multRel (COMPLEX,(z1 * z2)) by A1, XBOOLE_0:def 10; :: thesis: verum