---

Step * 1 of Lemma mset_prod_mem


1. g : DMon
2. a : MSet{g↓set}
3. b : MSet{g↓set}
4. u : |g|
⊢ u
  ∈b msFor{<MSet{g↓set},⋃,0>} u ∈ a
       msFor{<MSet{g↓set},⋃,0>} v ∈ b
         mset_inj{g↓set}(u * v) 
= ∃b{g↓set} v ∈ a
             ∃b{g↓set} w ∈ b
                        (u =b (v * w))
BY
{ ((RewriteWith [] `` 
  mset_mem_mon_for_union 
  mset_mem_char 
  mset_for_mset_inj`` 0) THENA Auto) }

1
1. g : DMon
2. a : MSet{g↓set}
3. b : MSet{g↓set}
4. u : |g|
⊢ ∃b{g↓set} u1 ∈ a. ∃b{g↓set} v ∈ b. ((u1 * v) (=b) u) = ∃b{g↓set} v ∈ a. ∃b{g↓set} w ∈ b. (u =b (v * w))

---

Latex:

---

Latex:

1.  g  :  DMon
2.  a  :  MSet\{g\mdownarrow{}set\}
3.  b  :  MSet\{g\mdownarrow{}set\}
4.  u  :  |g|
\mvdash{}  u
    \mmember{}\msubb{}  msFor\{<MSet\{g\mdownarrow{}set\},\mcup{},0>\}  u  \mmember{}  a
              msFor\{<MSet\{g\mdownarrow{}set\},\mcup{},0>\}  v  \mmember{}  b
                  mset\_inj\{g\mdownarrow{}set\}(u  *  v) 
=  \mexists{}\msubb{}\{g\mdownarrow{}set\}  v  \mmember{}  a
                          \mexists{}\msubb{}\{g\mdownarrow{}set\}  w  \mmember{}  b
                                                (u  =\msubb{}  (v  *  w))


By

---

Latex:
((RewriteWith  []  `` 
    mset\_mem\_mon\_for\_union 
    mset\_mem\_char 
    mset\_for\_mset\_inj``  0)  THENA  Auto)

---

Home Index