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:19;
hence (S,n -bag ) . i = (S --> n) . i by A1, FUNCT_4:14
.= n by A1, FUNCOP_1:13 ;
:: thesis: verum