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
now :: thesis: for o being object st o in X holds
b . o = (({x},(b . x)) -bag) . o
let o be object ; :: thesis: ( o in X implies b . b1 = (({x},(b . x)) -bag) . b1 )
assume o in X ; :: thesis: b . b1 = (({x},(b . x)) -bag) . b1
per cases ( o = x or o <> x ) ;
suppose A: o = x ; :: thesis: b . b1 = (({x},(b . x)) -bag) . b1
then o in {x} by TARSKI:def 1;
hence b . o = (({x},(b . x)) -bag) . o by ; :: thesis: verum
end;
suppose o <> x ; :: thesis: (({x},(b . x)) -bag) . b1 = b . b1
then B: not o in {x} by TARSKI:def 1;
hence (({x},(b . x)) -bag) . o = 0 by UPROOTS:6
.= b . o by ;
:: thesis: verum
end;
end;
end;
hence b = ({x},(b . x)) -bag by PBOOLE:3; :: thesis: verum