let Z be non empty set ; :: thesis: for B being bag of Z
for o1, o2 being object st B . o1 = card B & o2 <> o1 holds
B . o2 = 0
let B be bag of Z; :: thesis: for o1, o2 being object st B . o1 = card B & o2 <> o1 holds
B . o2 = 0
let o1, o2 be object ; :: thesis: ( B . o1 = card B & o2 <> o1 implies B . o2 = 0 )
assume H: ( B . o1 = card B & o2 <> o1 ) ; :: thesis: B . o2 = 0

per cases ( B = EmptyBag Z or B <> EmptyBag Z ) ;

suppose B = EmptyBag Z ; :: thesis: B . o2 = 0

hence B . o2 = 0 by PBOOLE:5; :: thesis: verum

end;

suppose I: B <> EmptyBag Z ; :: thesis: B . o2 = 0

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 . o2 <> 0

assume AS: B . o2 <> 0 ; :: thesis: contradiction
then D1: o2 in support B by PRE_POLY:def 7;
then o2 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 = o2 ) by FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
G1: f . i = B . o2 by A, B, FUNCT_1:13;
card B <> 0 by I, UPROOTS:12;
then D2: o1 in support B by H, PRE_POLY:def 7;
then o1 in rng (canFS (support B)) by FUNCT_2:def 3;
then consider j being Nat such that
B2: ( j in dom (canFS (support B)) & (canFS (support B)) . j = o1 ) by FINSEQ_2:10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
(B . o1) + (B . o2) > (B . o1) + 0 by AS, XREAL_1:8;
then G2: (f . i) + (f . j) > card B by H, G1, A, B2, FUNCT_1:13;
support B c= dom B by PRE_POLY:37;
then ( i in dom f & j in dom f ) by A, B2, B, D1, D2, FUNCT_1:11;
hence contradiction by B2, B, A, H, G2, lembag2b; :: thesis: verum

end;

hence B . o2 = 0 ; :: thesis: verum

end;

end;