let A be set ; :: thesis: for b being Rbag of st b = EmptyBag A holds
Sum b = 0
let b be Rbag of ; :: 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:19;
then len (canFS (support b)) = 0 ;
then canFS (support b) = <*> NAT ;
then A1: b * (canFS (support b)) = <*> NAT ;
thus Sum b = 0 by A1, Def3, RVSUM_1:102; :: thesis: verum