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 b * (canFS (support b)) = <*> NAT ;

hence Sum b = 0 by Def2, RVSUM_1:72; :: thesis: verum

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 b * (canFS (support b)) = <*> NAT ;

hence Sum b = 0 by Def2, RVSUM_1:72; :: thesis: verum