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