let X be set ; :: thesis: for x being object
for b being bag of X holds support (b +* (x,0)) = (support b) \ {x}
let x be object ; :: thesis: for b being bag of X holds support (b +* (x,0)) = (support b) \ {x}
let b be bag of X; :: thesis: support (b +* (x,0)) = (support b) \ {x}
A1: ( dom (b +* (x,0)) = X & X = dom b ) by PARTFUN1:def 2;
thus support (b +* (x,0)) c= (support b) \ {x} :: according to XBOOLE_0:def 10 :: thesis: (support b) \ {x} c= support (b +* (x,0))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in support (b +* (x,0)) or y in (support b) \ {x} )
assume A2: y in support (b +* (x,0)) ; :: thesis: y in (support b) \ {x}
then A3: (b +* (x,0)) . y <> 0 by PRE_POLY:def 7;
A4: y <> x by A2, A3, A1, FUNCT_7:31;
then 0 <> b . y by A3, FUNCT_7:32;
then y in support b by PRE_POLY:def 7;
hence y in (support b) \ {x} by A4, ZFMISC_1:56; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (support b) \ {x} or y in support (b +* (x,0)) )
assume y in (support b) \ {x} ; :: thesis: y in support (b +* (x,0))
then A5: ( y in support b & support b c= dom b & x <> y ) by ZFMISC_1:56, PRE_POLY:37;
then ( 0 <> b . y & y in dom b ) by PRE_POLY:def 7;
then (b +* (x,0)) . y <> 0 by A5, FUNCT_7:32;
hence y in support (b +* (x,0)) by PRE_POLY:def 7; :: thesis: verum