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 FINSEQ_1:93;

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;

assume A18: b = (S,1) -bag ; :: thesis: ( S = support b & degree b = card S )

A19: rng (canFS S) = S by FUNCT_2:def 3;

thus S = support b by A18, Th5; :: thesis: degree b = card S

then degree b = Sum f by Def3;

hence degree b = (card S) * 1 by A22, RVSUM_1:80

.= card S ;

:: thesis: verum

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 FINSEQ_1:93;

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

rng f c= NAT
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, Def3;

A11: support b = support ((S,1) -bag) by A6, Th5;

end;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, Def3;

now :: thesis: for i being Element of NAT st i in dom F holds

F . i <> 0

then A10:
F = (len F) |-> 1
by A2, A5, A7, A8, A9, Th1;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 . ((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;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

A11: support b = support ((S,1) -bag) by A6, Th5;

now :: thesis: ( dom b = dom ((S,1) -bag) & ( for x being object st x in dom b holds

b . x = ((S,1) -bag) . x ) )

hence
b = (S,1) -bag
; :: thesis: verumb . x = ((S,1) -bag) . x ) )

thus
dom b = dom ((S,1) -bag)
by A1, PARTFUN1:def 2; :: thesis: for x being object st x in dom b holds

b . b_{2} = ((S,1) -bag) . b_{2}

let x be object ; :: thesis: ( x in dom b implies b . b_{1} = ((S,1) -bag) . b_{1} )

assume x in dom b ; :: thesis: b . b_{1} = ((S,1) -bag) . b_{1}

end;b . b

let x be object ; :: thesis: ( x in dom b implies b . b

assume x in dom b ; :: thesis: b . b

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

end;

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

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

:: thesis: verum

end;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, Th4 ;

:: thesis: verum

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

hence b . x =
0
by PRE_POLY:def 7

.= ((S,1) -bag) . x by A11, A15, PRE_POLY:def 7 ;

:: thesis: verum

end;.= ((S,1) -bag) . x by A11, A15, PRE_POLY:def 7 ;

:: thesis: verum

proof

then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
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: y in NAT

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 . ((canFS S) . x) by A16, FUNCT_1:12;

hence y in NAT by A17; :: thesis: verum

end;assume y in rng f ; :: thesis: y in NAT

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 . ((canFS S) . x) by A16, FUNCT_1:12;

hence y in NAT by A17; :: thesis: verum

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

then A22:
f = (card S) |-> 1
by FINSEQ_2:9;f . i = ((card S) |-> 1) . i ) )

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, Th4, FUNCT_1:3

.= ((card S) |-> 1) . i by A20, A21, FUNCOP_1:7 ;

:: thesis: verum

end;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, Th4, FUNCT_1:3

.= ((card S) |-> 1) . i by A20, A21, FUNCOP_1:7 ;

:: thesis: verum

thus S = support b by A18, Th5; :: thesis: degree b = card S

then degree b = Sum f by Def3;

hence degree b = (card S) * 1 by A22, RVSUM_1:80

.= card S ;

:: thesis: verum