let U1, U2, 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;

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 :: thesis: for x being object st x in n -placesOf (P * Q) holds

x in (n -placesOf P) * (n -placesOf Q)

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

let x be object ; :: 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

A1: ( x = [p,q] & ( for j being set st j in Seg n holds

[(p . j),(q . j)] in P * Q ) ) ;

defpred S_{1}[ set , set ] means ( [(p . $1),$2] in P & [$2,(q . $1)] in Q );

A2: for k being Nat st k in Seg n holds

ex y being Element of U st S_{1}[k,y]

A4: ( dom r = Seg n & ( for k being Nat st k in Seg n holds

S_{1}[k,r . k] ) )
from FINSEQ_1:sch 5(A2);

len r = nn by FINSEQ_1:def 3, A4;

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 A4;

then A5: [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 A4;

then [rrrr,q] in n -placesOf Q ;

hence x in (n -placesOf P) * (n -placesOf Q) by A1, A5, RELAT_1:def 8; :: thesis: verum

end;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

A1: ( x = [p,q] & ( for j being set st j in Seg n holds

[(p . j),(q . j)] in P * Q ) ) ;

defpred S

A2: for k being Nat st k in Seg n holds

ex y being Element of U st S

proof

consider r being FinSequence of U such that
let k be Nat; :: thesis: ( k in Seg n implies ex y being Element of U st S_{1}[k,y] )

assume k in Seg n ; :: thesis: ex y being Element of U st S_{1}[k,y]

then [(p . k),(q . k)] in P * Q by A1;

then consider y being object such that

A3: ( [(p . k),y] in P & [y,(q . k)] in Q ) by RELAT_1:def 8;

( y in rng P & rng P c= U ) by A3, XTUPLE_0:def 13;

then reconsider yy = y as Element of U ;

take yy ; :: thesis: S_{1}[k,yy]

thus S_{1}[k,yy]
by A3; :: thesis: verum

end;assume k in Seg n ; :: thesis: ex y being Element of U st S

then [(p . k),(q . k)] in P * Q by A1;

then consider y being object such that

A3: ( [(p . k),y] in P & [y,(q . k)] in Q ) by RELAT_1:def 8;

( y in rng P & rng P c= U ) by A3, XTUPLE_0:def 13;

then reconsider yy = y as Element of U ;

take yy ; :: thesis: S

thus S

A4: ( dom r = Seg n & ( for k being Nat st k in Seg n holds

S

len r = nn by FINSEQ_1:def 3, A4;

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 A4;

then A5: [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 A4;

then [rrrr,q] in n -placesOf Q ;

hence x in (n -placesOf P) * (n -placesOf Q) by A1, A5, RELAT_1:def 8; :: thesis: verum