let U1, U2, 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;
A1: ( 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 Lm12;

let t be object ; :: thesis:
assume A2: t in (n -placesOf P) * (n -placesOf Q) ; :: thesis:
then consider x, z being object such that
A3: t = [x,z] by RELAT_1:def 1;
consider y being object such that
A4: ( [x,y] in n -placesOf P & [y,z] in n -placesOf Q ) by A3, A2, RELAT_1:def 8;
consider p1 being Element of n -tuples_on U1, p2 being Element of n -tuples_on U such that
A5: ( [p1,p2] = [x,y] & p2 c= p1 * P ) by A1, A4;
consider q1 being Element of n -tuples_on U2, q2 being Element of n -tuples_on U3 such that
A6: ( [q1,q2] = [y,z] & q2 c= q1 * Q ) by A1, A4;
A7: ( p2 * Q c= (p1 * P) * Q & p1 = x & p2 = y & q1 = y & q2 = z ) by XTUPLE_0:1, RELAT_1:30, A5, A6;
then q2 c= (p1 * P) * Q by XBOOLE_1:1, A6;
then ( [p1,q2] = [p1,q2] & q2 c= p1 * (P * Q) ) by RELAT_1:36;
hence t in n -placesOf (P * Q) by A3, A7, A1; :: thesis:

end;