let X be non empty set ; :: thesis: for A being finite Subset of X
for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A
let A be finite Subset of X; :: thesis: for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A
let R be being_linear-order Order of X; :: thesis: len (SgmX (R,A)) = card A
( field R = X & R linearly_orders field R ) by ORDERS_1:15, ORDERS_1:37;
hence len (SgmX (R,A)) = card A by ORDERS_1:38, PRE_POLY:11; :: thesis: verum