let X be set ; :: thesis: for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
SgmX R,A is one-to-one
let A be finite Subset of X; :: thesis: for R being Order of X st R linearly_orders A holds
SgmX R,A is one-to-one
let R be Order of X; :: thesis: ( R linearly_orders A implies SgmX R,A is one-to-one )
assume A1: R linearly_orders A ; :: thesis: SgmX R,A is one-to-one
set f = SgmX R,A;
consider s1' being Subset of X such that
A2: ( s1' = A & R linearly_orders s1' ) by A1;
rng (SgmX R,A) = A by A2, Def2;
then reconsider f = SgmX R,A as FinSequence of A by FINSEQ_1:def 4;
reconsider f = f as FinSequence of RelStr(# A,(R |_2 A) #) ;
f is one-to-one

proof

let k, l be set ; :: according to FUNCT_1:def 8 :: thesis: ( not k in dom f or not l in dom f or not f . k = f . l or k = l )
assume A3: ( k in dom f & l in dom f & f . k = f . l ) ; :: thesis: k = l
then reconsider k = k, l = l as Element of NAT ;
reconsider fk = f . k as Element of RelStr(# A,(R |_2 A) #) by A3, FINSEQ_2:13;
reconsider fl = f . l as Element of RelStr(# A,(R |_2 A) #) by A3, FINSEQ_2:13;
A4: ( fk = f /. k & fl = f /. l ) by A3, PARTFUN1:def 8;

now

assume A5: k <> l ; :: thesis: contradiction
A6: f /. k = f . k by A3, PARTFUN1:def 8
.= (SgmX R,A) /. k by A3, PARTFUN1:def 8 ;
A7: f /. l = f . l by A3, PARTFUN1:def 8
.= (SgmX R,A) /. l by A3, PARTFUN1:def 8 ;

per cases ( k < l or l < k ) by A5, XXREAL_0:1;

suppose k < l ; :: thesis: contradiction

hence contradiction by A2, A3, A4, A6, A7, Def2; :: thesis: verum

end;

suppose l < k ; :: thesis: contradiction

hence contradiction by A2, A3, A4, A6, A7, Def2; :: thesis: verum

end;

end;

end;

hence k = l ; :: thesis: verum

end;

hence SgmX R,A is one-to-one ; :: thesis: verum