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

for R being Relation of U1,U2 holds n -placesOf (R ~) = (n -placesOf R) ~

let n be Nat; :: thesis: for R being Relation of U1,U2 holds n -placesOf (R ~) = (n -placesOf R) ~

let R be Relation of U1,U2; :: thesis: n -placesOf (R ~) = (n -placesOf R) ~

set N1 = n -tuples_on U1;

set N2 = n -tuples_on U2;

set IT = { [q,p] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : for j being set st j in Seg n holds

[(p . j),(q . j)] in R } ;

reconsider Q = R ~ as Relation of U2,U1 ;

reconsider Rn = n -placesOf R as Relation of (n -tuples_on U1),(n -tuples_on U2) ;

reconsider LH = n -placesOf Q as Relation of (n -tuples_on U2),(n -tuples_on U1) ;

reconsider RH = Rn ~ as Relation of (n -tuples_on U2),(n -tuples_on U1) ;

then (RH ~) \ (LH ~) = {} ;

then (RH \ LH) ~ = {} by RELAT_1:24;

then ((RH \ LH) ~) ~ = {} ;

then RH c= LH by XBOOLE_1:37;

hence n -placesOf (R ~) = (n -placesOf R) ~ by A2; :: thesis: verum

for R being Relation of U1,U2 holds n -placesOf (R ~) = (n -placesOf R) ~

let n be Nat; :: thesis: for R being Relation of U1,U2 holds n -placesOf (R ~) = (n -placesOf R) ~

let R be Relation of U1,U2; :: thesis: n -placesOf (R ~) = (n -placesOf R) ~

set N1 = n -tuples_on U1;

set N2 = n -tuples_on U2;

set IT = { [q,p] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : for j being set st j in Seg n holds

[(p . j),(q . j)] in R } ;

reconsider Q = R ~ as Relation of U2,U1 ;

reconsider Rn = n -placesOf R as Relation of (n -tuples_on U1),(n -tuples_on U2) ;

reconsider LH = n -placesOf Q as Relation of (n -tuples_on U2),(n -tuples_on U1) ;

reconsider RH = Rn ~ as Relation of (n -tuples_on U2),(n -tuples_on U1) ;

now :: thesis: for x being object st x in LH holds

x in RH

then A2:
LH c= RH
by TARSKI:def 3;x in RH

let x be object ; :: thesis: ( x in LH implies x in RH )

assume x in LH ; :: thesis: x in RH

then consider p being Element of n -tuples_on U2, q being Element of n -tuples_on U1 such that

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

[(p . j),(q . j)] in R ~ ) ) ;

for j being set st j in Seg n holds

[(q . j),(p . j)] in R

hence x in RH by RELAT_1:def 7, A1; :: thesis: verum

end;assume x in LH ; :: thesis: x in RH

then consider p being Element of n -tuples_on U2, q being Element of n -tuples_on U1 such that

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

[(p . j),(q . j)] in R ~ ) ) ;

for j being set st j in Seg n holds

[(q . j),(p . j)] in R

proof

then
[q,p] in Rn
;
let j be set ; :: thesis: ( j in Seg n implies [(q . j),(p . j)] in R )

assume j in Seg n ; :: thesis: [(q . j),(p . j)] in R

then [(p . j),(q . j)] in R ~ by A1;

hence [(q . j),(p . j)] in R by RELAT_1:def 7; :: thesis: verum

end;assume j in Seg n ; :: thesis: [(q . j),(p . j)] in R

then [(p . j),(q . j)] in R ~ by A1;

hence [(q . j),(p . j)] in R by RELAT_1:def 7; :: thesis: verum

hence x in RH by RELAT_1:def 7, A1; :: thesis: verum

now :: thesis: for x being object st x in RH ~ holds

x in LH ~

then
RH ~ c= LH ~
by TARSKI:def 3;x in LH ~

let x be object ; :: thesis: ( x in RH ~ implies x in LH ~ )

assume x in RH ~ ; :: thesis: x in LH ~

then consider p being Element of n -tuples_on U1, q being Element of n -tuples_on U2 such that

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

[(p . j),(q . j)] in R ) ) ;

for j being set st j in Seg n holds

[(q . j),(p . j)] in R ~

hence x in LH ~ by A3, RELAT_1:def 7; :: thesis: verum

end;assume x in RH ~ ; :: thesis: x in LH ~

then consider p being Element of n -tuples_on U1, q being Element of n -tuples_on U2 such that

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

[(p . j),(q . j)] in R ) ) ;

for j being set st j in Seg n holds

[(q . j),(p . j)] in R ~

proof

then
[q,p] in LH
;
let j be set ; :: thesis: ( j in Seg n implies [(q . j),(p . j)] in R ~ )

assume j in Seg n ; :: thesis: [(q . j),(p . j)] in R ~

then [(p . j),(q . j)] in R by A3;

hence [(q . j),(p . j)] in R ~ by RELAT_1:def 7; :: thesis: verum

end;assume j in Seg n ; :: thesis: [(q . j),(p . j)] in R ~

then [(p . j),(q . j)] in R by A3;

hence [(q . j),(p . j)] in R ~ by RELAT_1:def 7; :: thesis: verum

hence x in LH ~ by A3, RELAT_1:def 7; :: thesis: verum

then (RH ~) \ (LH ~) = {} ;

then (RH \ LH) ~ = {} by RELAT_1:24;

then ((RH \ LH) ~) ~ = {} ;

then RH c= LH by XBOOLE_1:37;

hence n -placesOf (R ~) = (n -placesOf R) ~ by A2; :: thesis: verum