let U1, U2 be non empty set ; 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; 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; 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 H1( set , set ) -> object = [$1,$2];
defpred S1[ Function, Function] means for j being set st j in Seg n holds
[($1 . j),($2 . j)] in R;
defpred S2[ 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 = { H1(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S1[p,q] } ;
set RH = { H1(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S2[p,q] } ;
A1:
for u being Element of n -tuples_on U1
for v being Element of n -tuples_on U2 holds
( S1[u,v] iff S2[u,v] )
proof
let u be
Element of
n -tuples_on U1;
for v being Element of n -tuples_on U2 holds
( S1[u,v] iff S2[u,v] )let v be
Element of
n -tuples_on U2;
( S1[u,v] iff S2[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
(
S1[
u,
v] implies
S2[
u,
v] )
( S2[u,v] implies S1[u,v] )
assume A7:
S2[
u,
v]
;
S1[u,v]
now for j being set st j in Seg n holds
[(u . j),(v . j)] in Rlet j be
set ;
( j in Seg n implies [(u . j),(v . j)] in R )assume A8:
j in Seg n
;
[(u . j),(v . j)] in Rthen 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;
verum end;
hence
S1[
u,
v]
;
verum
end;
{ H1(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S1[p,q] } = { H1(p,q) where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : S2[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 }
; verum