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 )
set f = SgmX (R,A);
A1: dom (SgmX (R,A)) = Seg (len (SgmX (R,A))) by FINSEQ_1:def 3;
A2: card (Seg (len (SgmX (R,A)))) = card (len (SgmX (R,A))) by CARD_1:5, FINSEQ_1:54;
assume A3: R linearly_orders A ; :: thesis: len (SgmX (R,A)) = card A
then A4: SgmX (R,A) is one-to-one by Th9;
rng (SgmX (R,A)) = A by A3, Def2;
hence len (SgmX (R,A)) = card A by A2, A1, A4, CARD_1:5, WELLORD2:def 4; :: thesis: verum