let X be set ; :: thesis: for S being finite Subset of X

for n being Element of NAT st ( S is empty or n = 0 ) holds

(S,n) -bag = EmptyBag X

let S be finite Subset of X; :: thesis: for n being Element of NAT st ( S is empty or n = 0 ) holds

(S,n) -bag = EmptyBag X

let n be Element of NAT ; :: thesis: ( ( S is empty or n = 0 ) implies (S,n) -bag = EmptyBag X )

assume A1: ( S is empty or n = 0 ) ; :: thesis: (S,n) -bag = EmptyBag X

for n being Element of NAT st ( S is empty or n = 0 ) holds

(S,n) -bag = EmptyBag X

let S be finite Subset of X; :: thesis: for n being Element of NAT st ( S is empty or n = 0 ) holds

(S,n) -bag = EmptyBag X

let n be Element of NAT ; :: thesis: ( ( S is empty or n = 0 ) implies (S,n) -bag = EmptyBag X )

assume A1: ( S is empty or n = 0 ) ; :: thesis: (S,n) -bag = EmptyBag X

now :: thesis: for i being object st i in X holds

((S,n) -bag) . i = (EmptyBag X) . i

hence
(S,n) -bag = EmptyBag X
by PBOOLE:3; :: thesis: verum((S,n) -bag) . i = (EmptyBag X) . i

let i be object ; :: thesis: ( i in X implies ((S,n) -bag) . b_{1} = (EmptyBag X) . b_{1} )

assume i in X ; :: thesis: ((S,n) -bag) . b_{1} = (EmptyBag X) . b_{1}

end;assume i in X ; :: thesis: ((S,n) -bag) . b