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 ;
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 ;
then ( n = 1 & m = 1 ) by ;
hence contradiction by A5; :: thesis: verum
end;
hence SgmX (R,B) = <*x*> by ; :: thesis: verum