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;
Seg (len (SgmX R,A)), len (SgmX R,A) are_equipotent by FINSEQ_1:75;
then A2: card (Seg (len (SgmX R,A))) = card (len (SgmX R,A)) by CARD_1:21;
assume A3: R linearly_orders A ; :: thesis: len (SgmX R,A) = card A
then A4: SgmX R,A is one-to-one by Th8T;
rng (SgmX R,A) = A by A3, Def2T;
then Seg (len (SgmX R,A)),A are_equipotent by A1, A4, WELLORD2:def 4;
hence len (SgmX R,A) = card A by A2, CARD_1:21; :: thesis: verum