let z be Complex; :: thesis: for X, Y being complex-membered set holds multRel ((X /\ Y),z) = (multRel (X,z)) /\ (multRel (Y,z))
let X, Y be complex-membered set ; :: thesis: multRel ((X /\ Y),z) = (multRel (X,z)) /\ (multRel (Y,z))

now :: thesis: for z0 being object holds
( ( z0 in multRel ((X /\ Y),z) implies ( z0 in multRel (X,z) & z0 in multRel (Y,z) ) ) & ( z0 in multRel (X,z) & z0 in multRel (Y,z) implies z0 in multRel ((X /\ Y),z) ) )

let z0 be object ; :: thesis: ( ( z0 in multRel ((X /\ Y),z) implies ( z0 in multRel (X,z) & z0 in multRel (Y,z) ) ) & ( z0 in multRel (X,z) & z0 in multRel (Y,z) implies z0 in multRel ((X /\ Y),z) ) )

hereby :: thesis: ( z0 in multRel (X,z) & z0 in multRel (Y,z) implies z0 in multRel ((X /\ Y),z) )

assume A1: z0 in multRel ((X /\ Y),z) ; :: thesis: ( z0 in multRel (X,z) & z0 in multRel (Y,z) )
then consider x, y being object such that
A2: z0 = [x,y] by RELAT_1:def 1;
reconsider a = x, b = y as set by TARSKI:1;
[a,b] in multRel ((X /\ Y),z) by A1, A2;
then ( a in X /\ Y & b in X /\ Y ) by MMLQUER2:4;
then reconsider a = a, b = b as Complex ;
[a,b] in multRel ((X /\ Y),z) by A1, A2;
then ( a in X /\ Y & b in X /\ Y & b = z * a ) by Th42;
then ( a in X & b in X & a in Y & b in Y & b = z * a ) by XBOOLE_0:def 4;
hence ( z0 in multRel (X,z) & z0 in multRel (Y,z) ) by A2, Th42; :: thesis: verum

end;

assume A3: ( z0 in multRel (X,z) & z0 in multRel (Y,z) ) ; :: thesis: z0 in multRel ((X /\ Y),z)
then consider x, y being object such that
A4: z0 = [x,y] by RELAT_1:def 1;
reconsider a = x, b = y as set by TARSKI:1;
[a,b] in multRel (X,z) by A3, A4;
then ( a in X & b in X ) by MMLQUER2:4;
then reconsider a = a, b = b as Complex ;
( [a,b] in multRel (X,z) & [a,b] in multRel (Y,z) ) by A3, A4;
then ( a in X & b in X & a in Y & b in Y & b = z * a ) by Th42;
then ( a in X /\ Y & b in X /\ Y & b = z * a ) by XBOOLE_0:def 4;
hence z0 in multRel ((X /\ Y),z) by A4, Th42; :: thesis: verum

end;

hence multRel ((X /\ Y),z) = (multRel (X,z)) /\ (multRel (Y,z)) by XBOOLE_0:def 4; :: thesis: verum