let A be set ; :: thesis: Product (EmptyBag A) = 1
set b = EmptyBag A;
set cS = canFS (support (EmptyBag A));
support (EmptyBag A) = {} by BAGORDER:19;
then (EmptyBag A) * (canFS (support (EmptyBag A))) = <*> COMPLEX ;
hence Product (EmptyBag A) = 1 by Def5, RVSUM_1:124; :: thesis: verum