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:30 ;
rng (SgmX (R,A)) = A by A2, PRE_POLY:def 2;
hence SgmX (R,A) = <*a*> by A1, A3, FINSEQ_1:39; :: thesis: verum