let U1, U2 be non empty set ; :: thesis: for n being Nat

for R being Relation of U1,U2 holds n -placesOf R = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : q c= p * R }

let n be Nat; :: thesis: for R being Relation of U1,U2 holds n -placesOf R = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : q c= p * R }

let R be Relation of U1,U2; :: thesis: n -placesOf R = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : q c= p * R }

deffunc H_{1}( set , set ) -> object = [$1,$2];

defpred S_{1}[ Function, Function] means for j being set st j in Seg n holds

[($1 . j),($2 . j)] in R;

defpred S_{2}[ Relation, set ] means $2 c= $1 * R;

set N1 = n -tuples_on U1;

set N2 = n -tuples_on U2;

set D = Seg n;

set LH = { H_{1}(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S_{1}[p,q] } ;

set RH = { H_{1}(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S_{2}[p,q] } ;

A1: for u being Element of n -tuples_on U1

for v being Element of n -tuples_on U2 holds

( S_{1}[u,v] iff S_{2}[u,v] )
_{1}(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S_{1}[p,q] } = { H_{1}(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S_{2}[p,q] }
from FRAENKEL:sch 4(A1);

hence n -placesOf R = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : q c= p * R } ; :: thesis: verum

for R being Relation of U1,U2 holds n -placesOf R = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : q c= p * R }

let n be Nat; :: thesis: for R being Relation of U1,U2 holds n -placesOf R = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : q c= p * R }

let R be Relation of U1,U2; :: thesis: n -placesOf R = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : q c= p * R }

deffunc H

defpred S

[($1 . j),($2 . j)] in R;

defpred S

set N1 = n -tuples_on U1;

set N2 = n -tuples_on U2;

set D = Seg n;

set LH = { H

set RH = { H

A1: for u being Element of n -tuples_on U1

for v being Element of n -tuples_on U2 holds

( S

proof

{ H
let u be Element of n -tuples_on U1; :: thesis: for v being Element of n -tuples_on U2 holds

( S_{1}[u,v] iff S_{2}[u,v] )

let v be Element of n -tuples_on U2; :: thesis: ( S_{1}[u,v] iff S_{2}[u,v] )

A2: ( len u = n & len v = n ) by CARD_1:def 7;

then ( dom u = Seg n & dom v = Seg n ) by FINSEQ_1:def 3;

then A3: ( u = { [x,(u . x)] where x is Element of Seg n : x in Seg n } & v = { [x,(v . x)] where x is Element of Seg n : x in Seg n } ) by FOMODEL0:20;

thus ( S_{1}[u,v] implies S_{2}[u,v] )
:: thesis: ( S_{2}[u,v] implies S_{1}[u,v] )_{2}[u,v]
; :: thesis: S_{1}[u,v]

_{1}[u,v]
; :: thesis: verum

end;( S

let v be Element of n -tuples_on U2; :: thesis: ( S

A2: ( len u = n & len v = n ) by CARD_1:def 7;

then ( dom u = Seg n & dom v = Seg n ) by FINSEQ_1:def 3;

then A3: ( u = { [x,(u . x)] where x is Element of Seg n : x in Seg n } & v = { [x,(v . x)] where x is Element of Seg n : x in Seg n } ) by FOMODEL0:20;

thus ( S

proof

assume A7:
S
assume A4:
S_{1}[u,v]
; :: thesis: S_{2}[u,v]

_{2}[u,v]
by TARSKI:def 3; :: thesis: verum

end;now :: thesis: for z being object st z in v holds

z in u * R

hence
Sz in u * R

let z be object ; :: thesis: ( z in v implies z in u * R )

assume z in v ; :: thesis: z in u * R

then consider x being Element of Seg n such that

A5: ( z = [x,(v . x)] & x in Seg n ) by A3;

A6: [(u . x),(v . x)] in R by A4, A5;

[x,(u . x)] in u by A3, A5;

hence z in u * R by A5, A6, RELAT_1:def 8; :: thesis: verum

end;assume z in v ; :: thesis: z in u * R

then consider x being Element of Seg n such that

A5: ( z = [x,(v . x)] & x in Seg n ) by A3;

A6: [(u . x),(v . x)] in R by A4, A5;

[x,(u . x)] in u by A3, A5;

hence z in u * R by A5, A6, RELAT_1:def 8; :: thesis: verum

now :: thesis: for j being set st j in Seg n holds

[(u . j),(v . j)] in R

hence
S[(u . j),(v . j)] in R

let j be set ; :: thesis: ( j in Seg n implies [(u . j),(v . j)] in R )

assume A8: j in Seg n ; :: thesis: [(u . j),(v . j)] in R

then reconsider x = j as Element of Seg n ;

[x,(v . x)] in v by A3, A8;

then consider z being object such that

A9: ( [x,z] in u & [z,(v . x)] in R ) by A7, RELAT_1:def 8;

A10: z is set by TARSKI:1;

x in dom u by A2, FINSEQ_1:def 3, A8;

then z = u . x by A9, FUNCT_1:def 2, A10;

hence [(u . j),(v . j)] in R by A9; :: thesis: verum

end;assume A8: j in Seg n ; :: thesis: [(u . j),(v . j)] in R

then reconsider x = j as Element of Seg n ;

[x,(v . x)] in v by A3, A8;

then consider z being object such that

A9: ( [x,z] in u & [z,(v . x)] in R ) by A7, RELAT_1:def 8;

A10: z is set by TARSKI:1;

x in dom u by A2, FINSEQ_1:def 3, A8;

then z = u . x by A9, FUNCT_1:def 2, A10;

hence [(u . j),(v . j)] in R by A9; :: thesis: verum

hence n -placesOf R = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : q c= p * R } ; :: thesis: verum