let X be set ; :: thesis: for R being Order of X
for B being finite Subset of X
for x being object st B = {x} holds
SgmX (R,B) = <*x*>
let R be Order of X; :: thesis: for B being finite Subset of X
for x being object st B = {x} holds
SgmX (R,B) = <*x*>
let B be finite Subset of X; :: thesis: for x being object st B = {x} holds
SgmX (R,B) = <*x*>
let x be object ; :: thesis: ( B = {x} implies SgmX (R,B) = <*x*> )
assume A1: B = {x} ; :: thesis: SgmX (R,B) = <*x*>
set fin = <*x*>;
A2: rng <*x*> = B by A1, FINSEQ_1:38;
then reconsider fin = <*x*> as FinSequence of X by FINSEQ_1:def 4;
for n, m being Nat st n in dom fin & m in dom fin & n < m holds
( fin /. n <> fin /. m & [(fin /. n),(fin /. m)] in R )

proof

let n, m be Nat; :: thesis: ( n in dom fin & m in dom fin & n < m implies ( fin /. n <> fin /. m & [(fin /. n),(fin /. m)] in R ) )
assume that
A3: n in dom fin and
A4: m in dom fin and
A5: n < m ; :: thesis: ( fin /. n <> fin /. m & [(fin /. n),(fin /. m)] in R )
assume ( not fin /. n <> fin /. m or not [(fin /. n),(fin /. m)] in R ) ; :: thesis: contradiction
( n in Seg 1 & m in Seg 1 ) by A3, A4, FINSEQ_1:38;
then ( n = 1 & m = 1 ) by FINSEQ_1:2, TARSKI:def 1;
hence contradiction by A5; :: thesis: verum

end;

hence SgmX (R,B) = <*x*> by A2, PRE_POLY:9; :: thesis: verum