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

now :: thesis: for i being object st i in X holds
((S,n) -bag) . i = (EmptyBag X) . i

let i be object ; :: thesis: ( i in X implies ((S,n) -bag) . b₁ = (EmptyBag X) . b₁ )
assume i in X ; :: thesis: ((S,n) -bag) . b₁ = (EmptyBag X) . b₁

per cases ( i in S or not i in S ) ;

suppose i in S ; :: thesis: ((S,n) -bag) . b₁ = (EmptyBag X) . b₁

hence ((S,n) -bag) . i = 0 by A1, Th4
.= (EmptyBag X) . i by PBOOLE:5 ;
:: thesis: verum

end;

suppose not i in S ; :: thesis: ((S,n) -bag) . b₁ = (EmptyBag X) . b₁

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

end;

end;

end;

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