let n be non zero Nat; :: thesis: for X being non empty set

for x, y being Element of Funcs ((Seg n),X)

for R being Relation of X holds

( [x,y] in n -placesOf R iff for j being Element of Seg n holds [(x . j),(y . j)] in R )

let X be non empty set ; :: thesis: for x, y being Element of Funcs ((Seg n),X)

for R being Relation of X holds

( [x,y] in n -placesOf R iff for j being Element of Seg n holds [(x . j),(y . j)] in R )

let x, y be Element of Funcs ((Seg n),X); :: thesis: for R being Relation of X holds

( [x,y] in n -placesOf R iff for j being Element of Seg n holds [(x . j),(y . j)] in R )

let R be Relation of X; :: thesis: ( [x,y] in n -placesOf R iff for j being Element of Seg n holds [(x . j),(y . j)] in R )

reconsider xa = x as Element of n -tuples_on X by FINSEQ_2:93;

reconsider ya = y as Element of n -tuples_on X by FINSEQ_2:93;

thus ( [x,y] in n -placesOf R implies for j being Element of Seg n holds [(x . j),(y . j)] in R ) :: thesis: ( ( for j being Element of Seg n holds [(x . j),(y . j)] in R ) implies [x,y] in n -placesOf R )

for x, y being Element of Funcs ((Seg n),X)

for R being Relation of X holds

( [x,y] in n -placesOf R iff for j being Element of Seg n holds [(x . j),(y . j)] in R )

let X be non empty set ; :: thesis: for x, y being Element of Funcs ((Seg n),X)

for R being Relation of X holds

( [x,y] in n -placesOf R iff for j being Element of Seg n holds [(x . j),(y . j)] in R )

let x, y be Element of Funcs ((Seg n),X); :: thesis: for R being Relation of X holds

( [x,y] in n -placesOf R iff for j being Element of Seg n holds [(x . j),(y . j)] in R )

let R be Relation of X; :: thesis: ( [x,y] in n -placesOf R iff for j being Element of Seg n holds [(x . j),(y . j)] in R )

reconsider xa = x as Element of n -tuples_on X by FINSEQ_2:93;

reconsider ya = y as Element of n -tuples_on X by FINSEQ_2:93;

thus ( [x,y] in n -placesOf R implies for j being Element of Seg n holds [(x . j),(y . j)] in R ) :: thesis: ( ( for j being Element of Seg n holds [(x . j),(y . j)] in R ) implies [x,y] in n -placesOf R )

proof

thus
( ( for j being Element of Seg n holds [(x . j),(y . j)] in R ) implies [x,y] in n -placesOf R )
:: thesis: verum
assume
[x,y] in n -placesOf R
; :: thesis: for j being Element of Seg n holds [(x . j),(y . j)] in R

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

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

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

( x = p & y = q ) by A1, XTUPLE_0:1;

hence for j being Element of Seg n holds [(x . j),(y . j)] in R by A1; :: thesis: verum

end;then consider p, q being Element of n -tuples_on X such that

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

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

( x = p & y = q ) by A1, XTUPLE_0:1;

hence for j being Element of Seg n holds [(x . j),(y . j)] in R by A1; :: thesis: verum