let U2, U1, U3 be non empty set ; :: thesis: for n being Nat
for U being non empty Subset of U2
for P being Relation of U1,U
for Q being Relation of U2,U3 holds n -placesOf (P * Q) c= (n -placesOf P) * (n -placesOf Q)
let n be Nat; :: thesis: for U being non empty Subset of U2
for P being Relation of U1,U
for Q being Relation of U2,U3 holds n -placesOf (P * Q) c= (n -placesOf P) * (n -placesOf Q)
let U be non empty Subset of U2; :: thesis: for P being Relation of U1,U
for Q being Relation of U2,U3 holds n -placesOf (P * Q) c= (n -placesOf P) * (n -placesOf Q)
let P be Relation of U1,U; :: thesis: for Q being Relation of U2,U3 holds n -placesOf (P * Q) c= (n -placesOf P) * (n -placesOf Q)
let Q be Relation of U2,U3; :: thesis: n -placesOf (P * Q) c= (n -placesOf P) * (n -placesOf Q)
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;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;

now

let x be set ; :: thesis: ( x in n -placesOf (P * Q) implies x in (n -placesOf P) * (n -placesOf Q) )
assume x in n -placesOf (P * Q) ; :: thesis: x in (n -placesOf P) * (n -placesOf Q)
then consider p being Element of n -tuples_on U1, q being Element of n -tuples_on U3 such that
C0: ( x = [p,q] & ( for j being set st j in Seg n holds
[(p . j),(q . j)] in P * Q ) ) ;
defpred S₁[ set , set ] means ( [(p . $1),$2] in P & [$2,(q . $1)] in Q );
C1: for k being Nat st k in Seg n holds
ex y being Element of U st S₁[k,y]

proof

let k be Nat; :: thesis: ( k in Seg n implies ex y being Element of U st S₁[k,y] )
assume k in Seg n ; :: thesis: ex y being Element of U st S₁[k,y]
then [(p . k),(q . k)] in P * Q by C0;
then consider y being set such that
D0: ( [(p . k),y] in P & [y,(q . k)] in Q ) by RELAT_1:def 8;
( y in rng P & rng P c= U ) by D0, RELAT_1:def 5;
then reconsider yy = y as Element of U ;
take yy ; :: thesis: S₁[k,yy]
thus S₁[k,yy] by D0; :: thesis: verum

end;

consider r being FinSequence of U such that
C2: ( dom r = Seg n & ( for k being Nat st k in Seg n holds
S₁[k,r . k] ) ) from FINSEQ_1:sch 5(C1);
len r = nn by C2, FINSEQ_1:def 3;
then reconsider rr = r as n -element FinSequence of U by CARD_1:def 7;
reconsider rrr = rr as Element of n -tuples_on U by FOMODEL0:16;
reconsider rrrr = rrr as Element of n -tuples_on U2 by FOMODEL0:16;
( [p,rrr] = [p,rrr] & ( for j being set st j in Seg n holds
[(p . j),(rrr . j)] in P ) ) by C2;
then C4: [p,rrr] in n -placesOf P ;
( [rrrr,q] = [rrrr,q] & ( for j being set st j in Seg n holds
[(rrrr . j),(q . j)] in Q ) ) by C2;
then [rrrr,q] in n -placesOf Q ;
hence x in (n -placesOf P) * (n -placesOf Q) by C0, C4, RELAT_1:def 8; :: thesis: verum

end;

hence n -placesOf (P * Q) c= (n -placesOf P) * (n -placesOf Q) by TARSKI:def 3; :: thesis: verum