let A be finite Subset of SetPrimes; :: thesis: for i being object st i in support (A -bag) holds
(A -bag) . i = i
let i be object ; :: thesis: ( i in support (A -bag) implies (A -bag) . i = i )
assume aa: i in support (A -bag) ; :: thesis: (A -bag) . i = i
then A2: i in A by BagSupport;
A1: i in dom (id A) by aa, BagSupport;
(A -bag) . i = (id A) . i by A1, FUNCT_4:13
.= i by A2, FUNCT_1:17 ;
hence (A -bag) . i = i ; :: thesis: verum