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 object holds
( x in S iff ((S,n) -bag) . x <> 0 ) by Th3, Th4;
hence support ((S,n) -bag) = S by PRE_POLY:def 7; :: thesis: verum