---

Step * of Lemma mset_prod_mem

∀g:DMon. ∀a,b:MSet{g↓set}. ∀u:|g|.  u ∈b a × b = ∃b{g↓set} v ∈ a. ∃b{g↓set} w ∈ b. (u =b (v * w))
BY
{ ((RepD THENM Unfold `mset_prod` 0) THENA Auto) }

1
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))

---

Latex:

---

Latex:
\mforall{}g:DMon.  \mforall{}a,b:MSet\{g\mdownarrow{}set\}.  \mforall{}u:|g|.    u  \mmember{}\msubb{}  a  \mtimes{}  b  =  \mexists{}\msubb{}\{g\mdownarrow{}set\}  v  \mmember{}  a.  \mexists{}\msubb{}\{g\mdownarrow{}set\}  w  \mmember{}  b.  (u  =\msubb{}  (v  *  w))


By

---

Latex:
((RepD  THENM  Unfold  `mset\_prod`  0)  THENA  Auto)

---

Home Index