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;

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 )
;

end;

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;then support b = {} ;

hence card (({a},n) -bag) = n by X, bag1a; :: thesis: verum

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;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