let X be non empty set ; :: thesis: for b being bag of X
for a being Element of X holds (b \ a) + (({a},(b . a)) -bag) = b
let b be bag of X; :: thesis: for a being Element of X holds (b \ a) + (({a},(b . a)) -bag) = b
let a be Element of X; :: thesis: (b \ a) + (({a},(b . a)) -bag) = b
set c = (b \ a) + (({a},(b . a)) -bag);

now :: thesis: for o being object st o in X holds
((b \ a) + (({a},(b . a)) -bag)) . o = b . o

let o be object ; :: thesis: ( o in X implies ((b \ a) + (({a},(b . a)) -bag)) . b₁ = b . b₁ )
assume o in X ; :: thesis: ((b \ a) + (({a},(b . a)) -bag)) . b₁ = b . b₁
X: ((b \ a) + (({a},(b . a)) -bag)) . o = ((b \ a) . o) + ((({a},(b . a)) -bag) . o) by PRE_POLY:def 5;

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

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

then B: o in {a} by TARSKI:def 1;
thus ((b \ a) + (({a},(b . a)) -bag)) . o = 0 + ((({a},(b . a)) -bag) . o) by A, X, bb1
.= b . o by A, B, UPROOTS:7 ; :: thesis: verum

end;

suppose A: o <> a ; :: thesis: ((b \ a) + (({a},(b . a)) -bag)) . b₁ = b . b₁

then not o in {a} by TARSKI:def 1;
hence ((b \ a) + (({a},(b . a)) -bag)) . o = ((b \ a) . o) + 0 by X, UPROOTS:6
.= b . o by A, FUNCT_7:32 ;
:: thesis: verum

end;

end;

end;

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