let X be non empty set ; :: thesis: for b being bag of X

for x being Element of X st support b = {x} holds

b = ({x},(b . x)) -bag

let b be bag of X; :: thesis: for x being Element of X st support b = {x} holds

b = ({x},(b . x)) -bag

let x be Element of X; :: thesis: ( support b = {x} implies b = ({x},(b . x)) -bag )

assume AS: support b = {x} ; :: thesis: b = ({x},(b . x)) -bag

for x being Element of X st support b = {x} holds

b = ({x},(b . x)) -bag

let b be bag of X; :: thesis: for x being Element of X st support b = {x} holds

b = ({x},(b . x)) -bag

let x be Element of X; :: thesis: ( support b = {x} implies b = ({x},(b . x)) -bag )

assume AS: support b = {x} ; :: thesis: b = ({x},(b . x)) -bag

now :: thesis: for o being object st o in X holds

b . o = (({x},(b . x)) -bag) . o

hence
b = ({x},(b . x)) -bag
by PBOOLE:3; :: thesis: verumb . o = (({x},(b . x)) -bag) . o

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

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

end;assume o in X ; :: thesis: b . b