let Z be non empty set ; :: thesis: for B being bag of Z
for o being object holds B . o <= card B
let B be bag of Z; :: thesis: for o being object holds B . o <= card B
let o be object ; :: thesis: B . o <= card B
consider f being FinSequence of NAT such that
A: ( degree B = Sum f & f = B * (canFS (support B)) ) by UPROOTS:def 4;
set cS = canFS (support B);

now :: thesis: not B . o > card B

assume AS: B . o > card B ; :: thesis: contradiction
then o in support B by PRE_POLY:def 7;
then o in rng (canFS (support B)) by FUNCT_2:def 3;
then consider i being Nat such that
B: ( i in dom (canFS (support B)) & (canFS (support B)) . i = o ) by FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
f . i > card B by AS, A, B, FUNCT_1:13;
hence contradiction by A, NEWTON04:21; :: thesis: verum

end;

hence B . o <= card B ; :: thesis: verum