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 * ();
A1: dom b = A by PARTFUN1:def 2;
set g = (card S) |-> 1;
A2: len () = card S by FINSEQ_1:93;
A3: rng () = S by FUNCT_2:def 3;
then A4: dom (b * ()) = dom () by ;
then dom (b * ()) = Seg (len ()) by FINSEQ_1:def 3;
then reconsider f = b * () as FinSequence by FINSEQ_1:def 2;
A5: len () = len f by ;
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 * () by ;
now :: thesis: for i being Element of NAT st i in dom F holds
F . i <> 0
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 . (() . i) & () . i in rng () ) by ;
hence F . i <> 0 by ; :: thesis: verum
end;
then A10: F = (len F) |-> 1 by A2, A5, A7, A8, A9, Th1;
A11: support b = support ((S,1) -bag) by ;
now :: thesis: ( dom b = dom ((S,1) -bag) & ( for x being object st x in dom b holds
b . x = ((S,1) -bag) . x ) )
thus dom b = dom ((S,1) -bag) by ; :: thesis: for x being object st x in dom b holds
b . b2 = ((S,1) -bag) . b2

let x be object ; :: thesis: ( x in dom b implies b . b1 = ((S,1) -bag) . b1 )
assume x in dom b ; :: thesis: b . b1 = ((S,1) -bag) . b1
per cases ( x in support b or not x in support b ) ;
suppose A12: x in support b ; :: thesis: b . b1 = ((S,1) -bag) . b1
then A13: ((canFS S) ") . x in dom () by ;
then A14: ((canFS S) ") . x in Seg (len F) by ;
rng () = support b by ;
hence b . x = b . (() . ((() ") . x)) by
.= F . ((() ") . x) by
.= 1 by
.= ((S,1) -bag) . x by A6, A12, Th4 ;
:: thesis: verum
end;
suppose A15: not x in support b ; :: thesis: b . b1 = ((S,1) -bag) . b1
hence b . x = 0 by PRE_POLY:def 7
.= ((S,1) -bag) . x by ;
:: thesis: verum
end;
end;
end;
hence b = (S,1) -bag ; :: thesis: verum
end;
rng f c= NAT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis:
then consider x being object such that
A16: x in dom f and
A17: y = f . x by FUNCT_1:def 3;
f . x = b . (() . x) by ;
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 () = S by FUNCT_2:def 3;
now :: thesis: ( len f = card S & len ((card S) |-> 1) = card S & ( for i being Nat st i in dom f holds
f . i = ((card S) |-> 1) . i ) )
thus len f = card S by ; :: 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 ;
assume A21: i in dom f ; :: thesis: f . i = ((card S) |-> 1) . i
hence f . i = b . (() . i) by FUNCT_1:12
.= 1 by
.= ((card S) |-> 1) . i by ;
:: thesis: verum
end;
then A22: f = (card S) |-> 1 by FINSEQ_2:9;
thus S = support b by ; :: thesis:
then degree b = Sum f by Def3;
hence degree b = (card S) * 1 by
.= card S ;
:: thesis: verum