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 )

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

hence
SgmX (R,B) = <*x*>
by A2, PRE_POLY:9; :: thesis: verum
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;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