let n be Nat; :: thesis: for X being set
for x being object
for b being bag of X holds support (b +* (x,n)) c= {x} \/ (support b)
let X be set ; :: thesis: for x being object
for b being bag of X holds support (b +* (x,n)) c= {x} \/ (support b)
let x be object ; :: thesis: for b being bag of X holds support (b +* (x,n)) c= {x} \/ (support b)
let b be bag of X; :: thesis: support (b +* (x,n)) c= {x} \/ (support b)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in support (b +* (x,n)) or y in {x} \/ (support b) )
assume y in support (b +* (x,n)) ; :: thesis: y in {x} \/ (support b)
then A1: (b +* (x,n)) . y <> 0 by PRE_POLY:def 7;

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

suppose y = x ; :: thesis: y in {x} \/ (support b)

then y in {x} by TARSKI:def 1;
hence y in {x} \/ (support b) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose y <> x ; :: thesis: y in {x} \/ (support b)

then b . y <> 0 by A1, FUNCT_7:32;
then y in support b by PRE_POLY:def 7;
hence y in {x} \/ (support b) by XBOOLE_0:def 3; :: thesis: verum

end;

end;