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 . b₁ = (({x},(b . x)) -bag) . b₁ )
assume o in X ; :: thesis: b . b₁ = (({x},(b . x)) -bag) . b₁

per cases ( o = x or o <> x ) ;

suppose A: o = x ; :: thesis: b . b₁ = (({x},(b . x)) -bag) . b₁

then o in {x} by TARSKI:def 1;
hence b . o = (({x},(b . x)) -bag) . o by A, UPROOTS:7; :: thesis: verum

end;

suppose o <> x ; :: thesis: (({x},(b . x)) -bag) . b₁ = b . b₁

then B: not o in {x} by TARSKI:def 1;
hence (({x},(b . x)) -bag) . o = 0 by UPROOTS:6
.= b . o by AS, B, PRE_POLY:def 7 ;
:: thesis: verum

end;

end;

end;

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