let A be finite Subset of SetPrimes; :: thesis: support (A -bag) = A
set f = A -bag ;
B1: support (A -bag) c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (A -bag) or x in A )
assume a10: x in support (A -bag) ; :: thesis: x in A
x in A

proof

assume not x in A ; :: thesis: contradiction
then not x in dom (id A) ;
then (A -bag) . x = (EmptyBag SetPrimes) . x by FUNCT_4:11
.= 0 by PBOOLE:5 ;
hence contradiction by a10, PRE_POLY:def 7; :: thesis: verum

end;

hence x in A ; :: thesis: verum

end;

A c= support (A -bag)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in support (A -bag) )
assume E1: x in A ; :: thesis: x in support (A -bag)
then x in dom (id A) ;
then (A -bag) . x = (id A) . x by FUNCT_4:13
.= x by E1, FUNCT_1:17 ;
then (A -bag) . x is Prime by NEWTON:def 6, E1;
hence x in support (A -bag) by PRE_POLY:def 7; :: thesis: verum

end;

hence support (A -bag) = A by B1, XBOOLE_0:def 10; :: thesis: verum