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)
B0: field r = X by ORDERS_1:12;
set R = n -placesOf r;
B2: field (n -placesOf r) = n -tuples_on X by ORDERS_1:12;

now

let x, y, z be set ; :: 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 C1: [x,y] in n -placesOf r ; :: thesis: ( [y,z] in n -placesOf r implies [x,z] in n -placesOf r )
assume C2: [y,z] in n -placesOf r ; :: thesis: [x,z] in n -placesOf r
C4: r is_transitive_in X by B0, RELAT_2:def 16;

now

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 Lm9, C1, C2;
hence [(xa . j),(za . j)] in r by C4, RELAT_2:def 8; :: thesis: verum

end;

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

end;

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