let n be Nat; :: thesis: for X being set
for b being bag of X st n <> 0 holds
support (n (#) b) = support b
let X be set ; :: thesis: for b being bag of X st n <> 0 holds
support (n (#) b) = support b
let b be bag of X; :: thesis: ( n <> 0 implies support (n (#) b) = support b )
assume A1: n <> 0 ; :: thesis: support (n (#) b) = support b
thus support (n (#) b) c= support b by Th7; :: according to XBOOLE_0:def 10 :: thesis: support b c= support (n (#) b)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support b or x in support (n (#) b) )
assume x in support b ; :: thesis: x in support (n (#) b)
then A2: b . x <> 0 by PRE_POLY:def 7;
(n (#) b) . x = n * (b . x) by VALUED_1:6;
hence x in support (n (#) b) by A1, A2, PRE_POLY:def 7; :: thesis: verum