---

Step * of Lemma prod_in_mset_prod

∀g:DMon. ∀a,b:MSet{g↓set}. ∀u,v:|g|.  ((↑(u ∈b a)) ⇒ (↑(v ∈b b)) ⇒ (↑((u * v) ∈b a × b)))
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|
5. v : |g|
6. ↑(u
∈b a)
7. ↑(v
∈b b)
⊢ ↑((u * v)
∈b msFor{<MSet{g↓set},⋃,0>} u ∈ a
     msFor{<MSet{g↓set},⋃,0>} v ∈ b
       mset_inj{g↓set}(u * v))

---

Latex:

---

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


By

---

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

---

Home Index