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₁( set , set ) -> object = [$1,$2];
defpred S₁[ Function, Function] means for j being set st j in Seg n holds
[($1 . j),($2 . j)] in R;
defpred S₂[ 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₁(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S₁[p,q] } ;
set RH = { H₁(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S₂[p,q] } ;
A1: for u being Element of n -tuples_on U1
for v being Element of n -tuples_on U2 holds
( S₁[u,v] iff S₂[u,v] )

proof

let u be Element of n -tuples_on U1; :: thesis: for v being Element of n -tuples_on U2 holds
( S₁[u,v] iff S₂[u,v] )
let v be Element of n -tuples_on U2; :: thesis: ( S₁[u,v] iff S₂[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₁[u,v] implies S₂[u,v] ) :: thesis: ( S₂[u,v] implies S₁[u,v] )

proof

assume A4: S₁[u,v] ; :: thesis: S₂[u,v]

now :: thesis: for z being object st z in v holds
z 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;

hence S₂[u,v] by TARSKI:def 3; :: thesis: verum

end;

assume A7: S₂[u,v] ; :: thesis: S₁[u,v]

now :: thesis: for j being set st j in Seg n holds
[(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;

hence S₁[u,v] ; :: thesis: verum

end;

{ H₁(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S₁[p,q] } = { H₁(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S₂[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