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) . b1 = (EmptyBag X) . b1 )
assume i in X ; :: thesis: ((S,n) -bag) . b1 = (EmptyBag X) . b1
per cases ( i in S or not i in S ) ;
suppose i in S ; :: thesis: ((S,n) -bag) . b1 = (EmptyBag X) . b1
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) . b1 = (EmptyBag X) . b1
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