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

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