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