let X be set ; :: thesis: for x being object
for i being Nat st x in X & i <> 0 holds
support ((EmptyBag X) +* (x,i)) = {x}
let x be object ; :: thesis: for i being Nat st x in X & i <> 0 holds
support ((EmptyBag X) +* (x,i)) = {x}
let i be Nat; :: thesis: ( x in X & i <> 0 implies support ((EmptyBag X) +* (x,i)) = {x} )
assume A1: ( x in X & i <> 0 ) ; :: thesis: support ((EmptyBag X) +* (x,i)) = {x}
reconsider i = i as Element of NAT by ORDINAL1:def 12;
reconsider D = X as non empty set by A1;
reconsider d = x as Element of D by A1;
(EmptyBag X) +* (x,i) = ({d},i) -bag by Th12;
hence support ((EmptyBag X) +* (x,i)) = {x} by A1, UPROOTS:8; :: thesis: verum