let X be set ; :: thesis: for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
len (SgmX R,A) = card A
let A be finite Subset of X; :: thesis: for R being Order of X st R linearly_orders A holds
len (SgmX R,A) = card A
let R be Order of X; :: thesis: ( R linearly_orders A implies len (SgmX R,A) = card A )
assume A1: R linearly_orders A ; :: thesis: len (SgmX R,A) = card A
set f = SgmX R,A;
consider s1' being Subset of X such that
A2: ( s1' = A & R linearly_orders s1' ) by A1;
( dom (SgmX R,A) = Seg (len (SgmX R,A)) & rng (SgmX R,A) = A & SgmX R,A is one-to-one ) by A2, Def2, Th8, FINSEQ_1:def 3;
then A3: ( Seg (len (SgmX R,A)),A are_equipotent & Seg (len (SgmX R,A)) is finite ) by WELLORD2:def 4;
Seg (len (SgmX R,A)), len (SgmX R,A) are_equipotent by FINSEQ_1:75;
then card (Seg (len (SgmX R,A))) = card (len (SgmX R,A)) by CARD_1:21;
hence len (SgmX R,A) = card A by A3, CARD_1:21; :: thesis: verum