let X be set ; :: thesis: for S being finite Subset of X
for n being Element of NAT st n <> 0 holds
support (S,n -bag ) = S
let S be finite Subset of X; :: thesis: for n being Element of NAT st n <> 0 holds
support (S,n -bag ) = S
let n be Element of NAT ; :: thesis: ( n <> 0 implies support (S,n -bag ) = S )
assume n <> 0 ; :: thesis: support (S,n -bag ) = S
then for x being set holds
( x in S iff (S,n -bag ) . x <> 0 ) by Th8, Th9;
hence support (S,n -bag ) = S by PRE_POLY:def 7; :: thesis: verum