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 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: f = SgmX (R,A)

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 that
A3: a in A and
A4: b in A and
A5: a <> b ; :: thesis: ( [a,b] in R or [b,a] in R )
consider n being Nat such that
A6: n in dom f and
A7: f . n = a by A1, A3, FINSEQ_2:11;
consider m being Nat such that
A8: m in dom f and
A9: f . m = b by A1, A4, FINSEQ_2:11;
A10: f /. m = f . m by A8, PARTFUN1:def 8;
A11: f /. n = f . n by A6, PARTFUN1:def 8;

now

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

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

suppose n = m ; :: thesis: contradiction

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

end;

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

now

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

suppose n > m ; :: thesis: contradiction

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

end;

suppose m > n ; :: thesis: contradiction

hence contradiction by A2, A6, A7, A8, A9, A11, A10, A12; :: 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 A15: R is_connected_in A by RELAT_2:def 6;
A16: field R = X by ORDERS_1:97;
then R is_antisymmetric_in X by RELAT_2:def 12;
then A17: R is_antisymmetric_in A by ORDERS_1:94;
R is_transitive_in X by A16, RELAT_2:def 16;
then A18: R is_transitive_in A by ORDERS_1:95;
R is_reflexive_in X by A16, RELAT_2:def 9;
then R is_reflexive_in A by ORDERS_1:93;
then R linearly_orders A by A17, A18, A15, ORDERS_1:def 8;
hence f = SgmX (R,A) by A1, A2, Def2T; :: thesis: verum