let z1, z2 be Complex; :: thesis: for X being complex-membered set holds (multRel (X,z1)) * (multRel (X,z2)) c= multRel (X,(z1 * z2))
let X be complex-membered set ; :: thesis: (multRel (X,z1)) * (multRel (X,z2)) c= multRel (X,(z1 * z2))

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

let x, y be object ; :: thesis: ( [x,y] in (multRel (X,z1)) * (multRel (X,z2)) implies [x,y] in multRel (X,(z1 * z2)) )
assume [x,y] in (multRel (X,z1)) * (multRel (X,z2)) ; :: thesis: [x,y] in multRel (X,(z1 * z2))
then consider z being object such that
A1: ( [x,z] in multRel (X,z1) & [z,y] in multRel (X,z2) ) by RELAT_1:def 8;
reconsider a = x, b = y, c = z as set by TARSKI:1;
( [a,c] in multRel (X,z1) & [c,b] in multRel (X,z2) ) by A1;
then A2: ( a in X & c in X & b in X ) by MMLQUER2:4;
then reconsider a = a, b = b, c = c as Complex ;
( c = z1 * a & b = z2 * c ) by A1, Th42;
then b = (z1 * z2) * a ;
hence [x,y] in multRel (X,(z1 * z2)) by A2, Th42; :: thesis: verum

end;

hence (multRel (X,z1)) * (multRel (X,z2)) c= multRel (X,(z1 * z2)) by RELAT_1:def 3; :: thesis: verum