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 )
proof
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;
thus ( ( for j being Element of Seg n holds [(x . j),(y . j)] in R ) implies [x,y] in n -placesOf R ) :: thesis: verum
proof
assume for j being Element of Seg n holds [(x . j),(y . j)] in R ; :: thesis: [x,y] in n -placesOf R
then for j being set st j in Seg n holds
[(xa . j),(ya . j)] in R ;
hence [x,y] in n -placesOf R ; :: thesis: verum
end;