let X be set ; :: thesis:
let A be finite Subset of X; :: thesis:
let R be Order of X; :: thesis:
let f be FinSequence of X; :: thesis:
assume that
A1: rng f = A and
A2: for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ; :: thesis:

now :: thesis:

let a, b be object ; :: thesis:
assume that
A3: a in A and
A4: b in A and
A5: a <> b ; :: thesis:
consider n being Nat such that
A6: n in dom f and
A7: f . n = a by A1, A3, FINSEQ_2:10;
consider m being Nat such that
A8: m in dom f and
A9: f . m = b by A1, A4, FINSEQ_2:10;
A10: f /. m = f . m by A8, PARTFUN1:def 6;
A11: f /. n = f . n by A6, PARTFUN1:def 6;

now :: thesis:

assume that
A12: not [a,b] in R and
A13: not [b,a] in R ; :: thesis:

per cases ;

suppose n = m ; :: thesis:

hence contradiction by A5, A7, A9; :: thesis:

end;

suppose A14: n <> m ; :: thesis:

now :: thesis:

per cases by A14, XXREAL_0:1;

suppose n > m ; :: thesis:

hence contradiction by A2, A6, A7, A8, A9, A11, A10, A13; :: thesis:

end;

suppose m > n ; :: thesis:

hence contradiction by A2, A6, A7, A8, A9, A11, A10, A12; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

hence ( [a,b] in R or [b,a] in R ) ; :: thesis:

end;

then A15: R is_connected_in A ;
A16: field R = X by ORDERS_1:12;
then A17: R is_antisymmetric_in A by ORDERS_1:9, RELAT_2:def 12;
R is_transitive_in X by A16, RELAT_2:def 16;
then A18: R is_transitive_in A ;
R is_reflexive_in X by A16, RELAT_2:def 9;
then R is_reflexive_in A ;
then R linearly_orders A by A17, A18, A15, ORDERS_1:def 9;
hence f = SgmX (R,A) by A1, A2, Def2; :: thesis: