let n be Nat; :: thesis: for X being set
for b being bag of X holds support (n (#) b) c= support b
let X be set ; :: thesis: for b being bag of X holds support (n (#) b) c= support b
let b be bag of X; :: thesis: support (n (#) b) c= support b
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (n (#) b) or x in support b )
assume A1: x in support (n (#) b) ; :: thesis: x in support b
(n (#) b) . x <> 0 by A1, PRE_POLY:def 7;
then x in dom (n (#) b) by FUNCT_1:def 2;
then (n (#) b) . x = n * (b . x) by VALUED_1:def 5;
then b . x <> 0 by A1, PRE_POLY:def 7;
hence x in support b by PRE_POLY:def 7; :: thesis: verum