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

let i be set ; :: 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, Th9
.= (EmptyBag X) . i by PRE_POLY:52 ;
:: thesis: verum

end;

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

hence (S,n -bag ) . i = 0 by Th8
.= (EmptyBag X) . i by PRE_POLY:52 ;
:: thesis: verum

end;

end;

end;

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