---

Step * 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
⊢ (x #∈ (a × b)) ≤ 1
BY
{ Unfold `mset_prod` 0 }

1
1. g : DMon@i'
2. a : FiniteSet{g↓set}@i
3. b : FiniteSet{g↓set}@i
4. x : |(g↓set)|@i
⊢ (x #∈ (msFor{<MSet{g↓set},⋃,0>} u ∈ a
           msFor{<MSet{g↓set},⋃,0>} v ∈ b
             mset_inj{g↓set}(u * v))) ≤ 1

---

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
\mvdash{}  (x  \#\mmember{}  (a  \mtimes{}  b))  \mleq{}  1


By

---

Latex:
Unfold  `mset\_prod`  0

---

Home Index