---

Step * 1 1 1 1 of Lemma prod_in_mset_prod


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)
8. ↑(u
∈b a)
9. ↑(v
∈b b)
⊢ ↑((u * v)
∈b mset_inj{g↓set}(u * v))
BY
{ xxx((RWW "mset_mem_char mset_for_mset_inj" 0  
THENM RWW "assert_of_mon_eq r*" 0 ) THEN Auto)⋅xxx }

---

Latex:

---

Latex:

1.  g  :  DMon
2.  a  :  MSet\{g\mdownarrow{}set\}
3.  b  :  MSet\{g\mdownarrow{}set\}
4.  u  :  |g|
5.  v  :  |g|
6.  \muparrow{}(u
\mmember{}\msubb{}  a)
7.  \muparrow{}(v
\mmember{}\msubb{}  b)
8.  \muparrow{}(u
\mmember{}\msubb{}  a)
9.  \muparrow{}(v
\mmember{}\msubb{}  b)
\mvdash{}  \muparrow{}((u  *  v)
\mmember{}\msubb{}  mset\_inj\{g\mdownarrow{}set\}(u  *  v))


By

---

Latex:
xxx((RWW  "mset\_mem\_char  mset\_for\_mset\_inj"  0   
THENM  RWW  "assert\_of\_mon\_eq  r*"  0  )  THEN  Auto)\mcdot{}xxx

---

Home Index