---

Step * 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
⊢ (x #∈ (msFor{<MSet{g↓set},⋃,0>} u ∈ a
           msFor{<MSet{g↓set},⋃,0>} v ∈ b
             mset_inj{g↓set}(u * v))) ≤ 1
BY
{ ((Backchain ``mset_count_bound_for_union``) THENA Auto) }

1
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

---

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{}  (msFor\{<MSet\{g\mdownarrow{}set\},\mcup{},0>\}  u  \mmember{}  a
                      msFor\{<MSet\{g\mdownarrow{}set\},\mcup{},0>\}  v  \mmember{}  b
                          mset\_inj\{g\mdownarrow{}set\}(u  *  v)))  \mleq{}  1


By

---

Latex:
((Backchain  ``mset\_count\_bound\_for\_union``)  THENA  Auto)

---

Home Index