set f = (EmptyBag SetPrimes) +* (id A);
dom ((EmptyBag SetPrimes) +* (id A)) = (dom (EmptyBag SetPrimes)) \/ (dom (id A)) by FUNCT_4:def 1
.= SetPrimes \/ (dom (id A)) by PARTFUN1:def 2
.= SetPrimes by XBOOLE_1:12 ;
then reconsider f = (EmptyBag SetPrimes) +* (id A) as ManySortedSet of SetPrimes by PARTFUN1:def 2, RELAT_1:def 18;
support f c= A

proof

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

proof

assume not x in A ; :: thesis: contradiction
then not x in dom (id A) ;
then f . 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;

hence (EmptyBag SetPrimes) +* (id A) is bag of SetPrimes by PRE_POLY:def 8; :: thesis: verum