let X be set ; :: thesis: for x being object
for b being bag of X holds b = (b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))
let x be object ; :: thesis: for b being bag of X holds b = (b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))
let b be bag of X; :: thesis: b = (b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))
set E = EmptyBag X;
set bx = b +* (x,0);
set Ex = (EmptyBag X) +* (x,(b . x));
A1: ( dom ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) = X & X = dom b & X = dom (EmptyBag X) ) by PARTFUN1:def 2;
for y being object st y in dom b holds
b . y = ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y

proof

let y be object ; :: thesis: ( y in dom b implies b . y = ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y )
assume A2: y in dom b ; :: thesis: b . y = ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y
A3: ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y = ((b +* (x,0)) . y) + (((EmptyBag X) +* (x,(b . x))) . y) by A2, A1, VALUED_1:def 1;

per cases ( ( x in X & x = y ) or ( x in X & x <> y ) or not x in X ) ;

suppose ( x in X & x = y ) ; :: thesis: b . y = ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y

then ( (b +* (x,0)) . y = 0 & ((EmptyBag X) +* (x,(b . x))) . y = b . y ) by A1, FUNCT_7:31;
hence b . y = ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y by A3; :: thesis: verum

end;

suppose ( x in X & x <> y ) ; :: thesis: b . y = ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y

then ( (b +* (x,0)) . y = b . y & ((EmptyBag X) +* (x,(b . x))) . y = (EmptyBag X) . y & (EmptyBag X) . y = 0 ) by FUNCT_7:32;
hence b . y = ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y by A3; :: thesis: verum

end;

suppose not x in X ; :: thesis: b . y = ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y

then ( b +* (x,0) = b & (EmptyBag X) +* (x,(b . x)) = EmptyBag X ) by A1, FUNCT_7:def 3;
hence b . y = ((b +* (x,0)) + ((EmptyBag X) +* (x,(b . x)))) . y by PRE_POLY:53; :: thesis: verum

end;

end;

end;

hence b = (b +* (x,0)) + ((EmptyBag X) +* (x,(b . x))) by A1; :: thesis: verum