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:100, ORDERS_1:133;
hence len (SgmX (R,A)) = card A by ORDERS_1:134, PRE_POLY:11; :: thesis: verum