let X be non empty set ; :: thesis: for a being Element of X
for n being Element of NAT holds card (({a},n) -bag) = n
let a be Element of X; :: thesis: for n being Element of NAT holds card (({a},n) -bag) = n
let n be Element of NAT ; :: thesis: card (({a},n) -bag) = n
reconsider b = ({a},n) -bag as bag of X ;
consider F being FinSequence of NAT such that
H: ( degree b = Sum F & F = b * (canFS (support b)) ) by UPROOTS:def 4;
I: a in {a} by TARSKI:def 1;
per cases ( n = 0 or n <> 0 ) ;
suppose X: n = 0 ; :: thesis: card (({a},n) -bag) = n
then b = EmptyBag X by UPROOTS:9;
then support b = {} ;
hence card (({a},n) -bag) = n by X, bag1a; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: card (({a},n) -bag) = n
then A: support b = {a} by UPROOTS:8;
then C: a in support b by TARSKI:def 1;
B: support b c= dom b by PRE_POLY:37;
F = b * <*a*> by A, H, FINSEQ_1:94
.= <*(b . a)*> by C, B, FINSEQ_2:34
.= <*n*> by I, UPROOTS:7 ;
hence card (({a},n) -bag) = n by H, RVSUM_1:73; :: thesis: verum
end;
end;