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