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

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