let X be set ; :: thesis: for A being finite Subset of X
for R being Order of X
for f being FinSequence of X st rng f = A & ( 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 ) ) holds
f = SgmX R,A
let A be finite Subset of X; :: thesis: for R being Order of X
for f being FinSequence of X st rng f = A & ( 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 ) ) holds
f = SgmX R,A
let R be Order of X; :: thesis: for f being FinSequence of X st rng f = A & ( 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 ) ) holds
f = SgmX R,A
let f be FinSequence of X; :: thesis: ( rng f = A & ( 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 ) ) implies f = SgmX R,A )
assume A1: ( rng f = A & ( 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: f = SgmX R,A
field R = X by ORDERS_1:97;
then ( R is_reflexive_in X & R is_antisymmetric_in X & R is_transitive_in X ) by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
then A2: ( R is_reflexive_in A & R is_antisymmetric_in A & R is_transitive_in A ) by ORDERS_1:93, ORDERS_1:94, ORDERS_1:95;

now

let a, b be set ; :: thesis: ( a in A & b in A & a <> b & not [a,b] in R implies [b,a] in R )
assume A3: ( a in A & b in A & a <> b ) ; :: thesis: ( [a,b] in R or [b,a] in R )
then consider n being Nat such that
A4: ( n in dom f & f . n = a ) by A1, FINSEQ_2:11;
consider m being Nat such that
A5: ( m in dom f & f . m = b ) by A1, A3, FINSEQ_2:11;
A6: ( f /. n = f . n & f /. m = f . m ) by A4, A5, PARTFUN1:def 8;

now

assume A7: ( not [a,b] in R & not [b,a] in R ) ; :: thesis: contradiction

per cases ( n = m or n <> m ) ;

suppose n = m ; :: thesis: contradiction

hence contradiction by A3, A4, A5; :: thesis: verum

end;

suppose A8: n <> m ; :: thesis: contradiction

now

per cases ( n > m or m > n ) by A8, XXREAL_0:1;

suppose n > m ; :: thesis: contradiction

hence contradiction by A1, A4, A5, A6, A7; :: thesis: verum

end;

suppose m > n ; :: thesis: contradiction

hence contradiction by A1, A4, A5, A6, A7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

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

end;

then R is_connected_in A by RELAT_2:def 6;
then R linearly_orders A by A2, ORDERS_1:def 8;
hence f = SgmX R,A by A1, Def2; :: thesis: verum