set S = SgmX ((BagOrder n),(Support p));

per cases ( p = 0_ (n,R) or p <> 0_ (n,R) ) ;

suppose p = 0_ (n,R) ; :: thesis: ( ( p <> 0_ (n,R) implies (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) is bag of n ) & ( not p <> 0_ (n,R) implies EmptyBag n is bag of n ) )

hence ( ( p <> 0_ (n,R) implies (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) is bag of n ) & ( not p <> 0_ (n,R) implies EmptyBag n is bag of n ) ) ; :: thesis: verum

end;

suppose I: p <> 0_ (n,R) ; :: thesis: ( ( p <> 0_ (n,R) implies (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) is bag of n ) & ( not p <> 0_ (n,R) implies EmptyBag n is bag of n ) )

field (BagOrder n) = Bags n by ORDERS_1:12;
then BagOrder n linearly_orders Support p by ORDERS_1:37, ORDERS_1:38;
then B: rng (SgmX ((BagOrder n),(Support p))) = Support p by PRE_POLY:def 2;
Support p <> {} by I, POLYNOM2:17;
then len (SgmX ((BagOrder n),(Support p))) >= 1 by FINSEQ_1:20;
then len (SgmX ((BagOrder n),(Support p))) in Seg (len (SgmX ((BagOrder n),(Support p)))) ;
then len (SgmX ((BagOrder n),(Support p))) in dom (SgmX ((BagOrder n),(Support p))) by FINSEQ_1:def 3;
then (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) in rng (SgmX ((BagOrder n),(Support p))) by FUNCT_1:3;
hence ( ( p <> 0_ (n,R) implies (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) is bag of n ) & ( not p <> 0_ (n,R) implies EmptyBag n is bag of n ) ) by B; :: thesis: verum

end;

end;