let n be non zero Nat; :: thesis: for X being non empty set
for r being total symmetric Relation of X holds n -placesOf r is total symmetric Relation of (n -tuples_on X)
let X be non empty set ; :: thesis: for r being total symmetric Relation of X holds n -placesOf r is total symmetric Relation of (n -tuples_on X)
let r be total symmetric Relation of X; :: thesis: n -placesOf r is total symmetric Relation of (n -tuples_on X)
A1: field r = X by ORDERS_1:12;
set R = n -placesOf r;
A2: field (n -placesOf r) = n -tuples_on X by ORDERS_1:12;
now :: thesis: for x, y being object st x in n -tuples_on X & y in n -tuples_on X & [x,y] in n -placesOf r holds
[y,x] in n -placesOf r
let x, y be object ; :: thesis: ( x in n -tuples_on X & y in n -tuples_on X & [x,y] in n -placesOf r implies [y,x] in n -placesOf r )
assume x in n -tuples_on X ; :: thesis: ( y in n -tuples_on X & [x,y] in n -placesOf r implies [y,x] in n -placesOf r )
then reconsider xa = x as Element of Funcs ((Seg n),X) by FINSEQ_2:93;
assume y in n -tuples_on X ; :: thesis: ( [x,y] in n -placesOf r implies [y,x] in n -placesOf r )
then reconsider ya = y as Element of Funcs ((Seg n),X) by FINSEQ_2:93;
assume A3: [x,y] in n -placesOf r ; :: thesis: [y,x] in n -placesOf r
now :: thesis: for j being Element of Seg n holds [(ya . j),(xa . j)] in r
let j be Element of Seg n; :: thesis: [(ya . j),(xa . j)] in r
( xa . j in X & ya . j in X & [(xa . j),(ya . j)] in r ) by Lm5, A3;
hence [(ya . j),(xa . j)] in r by RELAT_2:def 11, A1, RELAT_2:def 3; :: thesis: verum
end;
hence [y,x] in n -placesOf r by Lm5; :: thesis: verum
end;
hence n -placesOf r is total symmetric Relation of (n -tuples_on X) by RELAT_2:def 3, RELAT_2:def 11, A2; :: thesis: verum