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