let n be non zero Nat; :: thesis: for X being non empty set
for r being total transitive Relation of X holds n -placesOf r is total transitive Relation of (n -tuples_on X)
let X be non empty set ; :: thesis: for r being total transitive Relation of X holds n -placesOf r is total transitive Relation of (n -tuples_on X)
let r be total transitive Relation of X; :: thesis: n -placesOf r is total transitive 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, z being object st x in n -tuples_on X & y in n -tuples_on X & z in n -tuples_on X & [x,y] in n -placesOf r & [y,z] in n -placesOf r holds
[x,z] in n -placesOf r

let x, y, z be object ; :: thesis: ( x in n -tuples_on X & y in n -tuples_on X & z in n -tuples_on X & [x,y] in n -placesOf r & [y,z] in n -placesOf r implies [x,z] in n -placesOf r )
assume x in n -tuples_on X ; :: thesis: ( y in n -tuples_on X & z in n -tuples_on X & [x,y] in n -placesOf r & [y,z] in n -placesOf r implies [x,z] 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: ( z in n -tuples_on X & [x,y] in n -placesOf r & [y,z] in n -placesOf r implies [x,z] in n -placesOf r )
then reconsider ya = y as Element of Funcs ((Seg n),X) by FINSEQ_2:93;
assume z in n -tuples_on X ; :: thesis: ( [x,y] in n -placesOf r & [y,z] in n -placesOf r implies [x,z] in n -placesOf r )
then reconsider za = z as Element of Funcs ((Seg n),X) by FINSEQ_2:93;
assume A3: [x,y] in n -placesOf r ; :: thesis: ( [y,z] in n -placesOf r implies [x,z] in n -placesOf r )
assume A4: [y,z] in n -placesOf r ; :: thesis: [x,z] in n -placesOf r

now :: thesis: for j being Element of Seg n holds [(xa . j),(za . j)] in r

let j be Element of Seg n; :: thesis: [(xa . j),(za . j)] in r
( xa . j in X & ya . j in X & za . j in X & [(xa . j),(ya . j)] in r & [(ya . j),(za . j)] in r ) by Lm5, A3, A4;
hence [(xa . j),(za . j)] in r by A1, RELAT_2:def 8, RELAT_2:def 16; :: thesis: verum

end;

hence [x,z] in n -placesOf r by Lm5; :: thesis: verum

end;

hence n -placesOf r is total transitive Relation of (n -tuples_on X) by RELAT_2:def 8, RELAT_2:def 16, A2; :: thesis: verum