let A be set ; :: thesis: for b being Rbag of A st b = EmptyBag A holds
Sum b = 0
let b be Rbag of A; :: thesis: ( b = EmptyBag A implies Sum b = 0 )
set cS = canFS (support b);
assume b = EmptyBag A ; :: thesis: Sum b = 0
then support b = {} by BAGORDER:18;
then b * (canFS (support b)) = <*> NAT ;
hence Sum b = 0 by Def3, RVSUM_1:72; :: thesis: verum