let A be set ; :: thesis: for S being finite Subset of A
for b being bag of A holds
( ( S = support b & degree b = card S ) iff b = (S,1) -bag )
let S be finite Subset of A; :: thesis: for b being bag of A holds
( ( S = support b & degree b = card S ) iff b = (S,1) -bag )
let b be bag of A; :: thesis: ( ( S = support b & degree b = card S ) iff b = (S,1) -bag )
set cS = canFS S;
set f = b * (canFS S);
A1: dom b = A by PARTFUN1:def 2;
set g = (card S) |-> 1;
A2: len (canFS S) = card S by Th5;
A3: rng (canFS S) = S by FUNCT_2:def 3;
then A4: dom (b * (canFS S)) = dom (canFS S) by A1, RELAT_1:27;
then dom (b * (canFS S)) = Seg (len (canFS S)) by FINSEQ_1:def 3;
then reconsider f = b * (canFS S) as FinSequence by FINSEQ_1:def 2;
A5: len (canFS S) = len f by A4, FINSEQ_3:29;

hereby :: thesis: ( b = (S,1) -bag implies ( S = support b & degree b = card S ) )

set sb = (S,1) -bag ;
assume that
A6: S = support b and
A7: degree b = card S ; :: thesis: b = (S,1) -bag
consider F being FinSequence of NAT such that
A8: degree b = Sum F and
A9: F = b * (canFS S) by A6, Def4;

now

let i be Element of NAT ; :: thesis: ( i in dom F implies F . i <> 0 )
assume i in dom F ; :: thesis: F . i <> 0
then ( F . i = b . ((canFS S) . i) & (canFS S) . i in rng (canFS S) ) by A4, A9, FUNCT_1:3, FUNCT_1:12;
hence F . i <> 0 by A6, PRE_POLY:def 7; :: thesis: verum

end;

then A10: F = (len F) |-> 1 by A2, A5, A7, A8, A9, Th2;
A11: support b = support ((S,1) -bag) by A6, Th10;

now

thus dom b = dom ((S,1) -bag) by A1, PARTFUN1:def 2; :: thesis: for x being set st x in dom b holds
b . b₂ = ((S,1) -bag) . b₂
let x be set ; :: thesis: ( x in dom b implies b . b₁ = ((S,1) -bag) . b₁ )
assume x in dom b ; :: thesis: b . b₁ = ((S,1) -bag) . b₁

per cases ( x in support b or not x in support b ) ;

suppose A12: x in support b ; :: thesis: b . b₁ = ((S,1) -bag) . b₁

then A13: ((canFS S) ") . x in dom (canFS S) by A3, A6, FUNCT_1:32;
then A14: ((canFS S) ") . x in Seg (len F) by A4, A9, FINSEQ_1:def 3;
rng (canFS S) = support b by A6, FUNCT_2:def 3;
hence b . x = b . ((canFS S) . (((canFS S) ") . x)) by A12, FUNCT_1:35
.= F . (((canFS S) ") . x) by A9, A13, FUNCT_1:13
.= 1 by A10, A14, FUNCOP_1:7
.= ((S,1) -bag) . x by A6, A12, Th9 ;
:: thesis: verum

end;

suppose A15: not x in support b ; :: thesis: b . b₁ = ((S,1) -bag) . b₁

hence b . x = 0 by PRE_POLY:def 7
.= ((S,1) -bag) . x by A11, A15, PRE_POLY:def 7 ;
:: thesis: verum

end;

end;

end;

hence b = (S,1) -bag by FUNCT_1:2; :: thesis: verum

end;

rng f c= NAT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider x being set such that
A16: x in dom f and
A17: y = f . x by FUNCT_1:def 3;
f . x = b . ((canFS S) . x) by A16, FUNCT_1:12;
hence y in NAT by A17; :: thesis: verum

end;

then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
assume A18: b = (S,1) -bag ; :: thesis: ( S = support b & degree b = card S )
A19: rng (canFS S) = S by FUNCT_2:def 3;

now

thus len f = card S by A4, A2, FINSEQ_3:29; :: thesis: ( len ((card S) |-> 1) = card S & ( for i being Nat st i in dom f holds
f . i = ((card S) |-> 1) . i ) )
thus len ((card S) |-> 1) = card S by CARD_1:def 7; :: thesis: for i being Nat st i in dom f holds
f . i = ((card S) |-> 1) . i
let i be Nat; :: thesis: ( i in dom f implies f . i = ((card S) |-> 1) . i )
A20: dom f = Seg (card S) by A4, A2, FINSEQ_1:def 3;
assume A21: i in dom f ; :: thesis: f . i = ((card S) |-> 1) . i
hence f . i = b . ((canFS S) . i) by FUNCT_1:12
.= 1 by A4, A19, A18, A21, Th9, FUNCT_1:3
.= ((card S) |-> 1) . i by A20, A21, FUNCOP_1:7 ;
:: thesis: verum

end;

then A22: f = (card S) |-> 1 by FINSEQ_2:9;
thus S = support b by A18, Th10; :: thesis: degree b = card S
then degree b = Sum f by Def4;
hence degree b = (card S) * 1 by A22, RVSUM_1:80
.= card S ;
:: thesis: verum