let X be set ; :: thesis: for S being finite Subset of X
for n being Element of NAT
for i being object st not i in S holds
((S,n) -bag) . i = 0
let S be finite Subset of X; :: thesis: for n being Element of NAT
for i being object st not i in S holds
((S,n) -bag) . i = 0
let n be Element of NAT ; :: thesis: for i being object st not i in S holds
((S,n) -bag) . i = 0
let i be object ; :: thesis: ( not i in S implies ((S,n) -bag) . i = 0 )
assume A1: not i in S ; :: thesis: ((S,n) -bag) . i = 0
dom (S --> n) = S by FUNCOP_1:13;
hence ((S,n) -bag) . i = (EmptyBag X) . i by A1, FUNCT_4:11
.= 0 by PBOOLE:5 ;
:: thesis: verum