let X be set ; :: thesis: for a being Element of X
for A being finite Subset of X
for R being Order of X st A = {a} & R linearly_orders A holds
SgmX R,A = <*a*>
let a be Element of X; :: thesis: for A being finite Subset of X
for R being Order of X st A = {a} & R linearly_orders A holds
SgmX R,A = <*a*>
let A be finite Subset of X; :: thesis: for R being Order of X st A = {a} & R linearly_orders A holds
SgmX R,A = <*a*>
let R be Order of X; :: thesis: ( A = {a} & R linearly_orders A implies SgmX R,A = <*a*> )
assume that
A1: A = {a} and
A2: R linearly_orders A ; :: thesis: SgmX R,A = <*a*>
A3: len (SgmX R,A) = card A by A2, PRE_POLY:11
.= 1 by A1, CARD_1:50 ;
rng (SgmX R,A) = A by A2, PRE_POLY:def 2;
hence SgmX R,A = <*a*> by A1, A3, FINSEQ_1:56; :: thesis: verum