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

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