---

Step * 1 1 1 of Lemma mset_prod_wf2


1. g : DMon@i'
2. a : FiniteSet{g↓set}@i
3. b : FiniteSet{g↓set}@i
4. x : |(g↓set)|@i
5. u : |(g↓set)|@i
6. v : |(g↓set)|@i
⊢ (x #∈ mset_inj{g↓set}(u * v)) ≤ 1
BY
{ RWH (LemmaC `mset_count_inj`) 0 
THEN Auto' }

---

Latex:

---

Latex:

1.  g  :  DMon@i'
2.  a  :  FiniteSet\{g\mdownarrow{}set\}@i
3.  b  :  FiniteSet\{g\mdownarrow{}set\}@i
4.  x  :  |(g\mdownarrow{}set)|@i
5.  u  :  |(g\mdownarrow{}set)|@i
6.  v  :  |(g\mdownarrow{}set)|@i
\mvdash{}  (x  \#\mmember{}  mset\_inj\{g\mdownarrow{}set\}(u  *  v))  \mleq{}  1


By

---

Latex:
RWH  (LemmaC  `mset\_count\_inj`)  0 
THEN  Auto'

---

Home Index