let U2, U1, U3 be non empty set ; :: thesis:
let n be Nat; :: thesis:
let U be non empty Subset of U2; :: thesis:
let P be Relation of U1,U; :: thesis:
let Q be Relation of U2,U3; :: thesis:
set R = P * Q;
set LH = n -placesOf (P * Q);
set Pn = n -placesOf P;
set Qn = n -placesOf Q;
set RH = (n -placesOf P) * (n -placesOf Q);
set N = n -tuples_on U;
set N1 = n -tuples_on U1;
set N2 = n -tuples_on U2;
set N3 = n -tuples_on U3;
B0: ( n -placesOf (P * Q) = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U3 : q c= p * (P * Q) } & n -placesOf P = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U : q c= p * P } & n -placesOf Q = { [p,q] where p is Element of n -tuples_on U2, q is Element of n -tuples_on U3 : q c= p * Q } ) by Lm6;

let t be set ; :: thesis:
assume C6: t in (n -placesOf P) * (n -placesOf Q) ; :: thesis:
then consider x, z being set such that
C5: t = [x,z] by RELAT_1:def 1;
consider y being set such that
C0: ( [x,y] in n -placesOf P & [y,z] in n -placesOf Q ) by C5, C6, RELAT_1:def 8;
consider p1 being Element of n -tuples_on U1, p2 being Element of n -tuples_on U such that
C1: ( [p1,p2] = [x,y] & p2 c= p1 * P ) by B0, C0;
consider q1 being Element of n -tuples_on U2, q2 being Element of n -tuples_on U3 such that
C2: ( [q1,q2] = [y,z] & q2 c= q1 * Q ) by B0, C0;
C3: ( p2 * Q c= (p1 * P) * Q & p1 = x & p2 = y & q1 = y & q2 = z ) by C1, C2, RELAT_1:30, ZFMISC_1:27;
then q2 c= (p1 * P) * Q by C2, XBOOLE_1:1;
then ( [p1,q2] = [p1,q2] & q2 c= p1 * (P * Q) ) by RELAT_1:36;
hence t in n -placesOf (P * Q) by C5, C3, B0; :: thesis:

end;