let X be non empty set ; :: thesis: for A being finite Subset of
for R being being_linear-order Order of holds len (SgmX R,A) = card A
let A be finite Subset of ; :: thesis: for R being being_linear-order Order of holds len (SgmX R,A) = card A
let R be being_linear-order Order of ; :: 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