---

Step * 1 of Lemma mset_sum_ident_r


1. s : DSet@i'
2. a : MSet{s}@i
3. mset_mon{s} ∈ AbMon
⊢ (a + 0{s}) = a ∈ MSet{s}
BY
{ ((AddAllProperties 3 
THENM ARepD ["compound";"basic"] 
THENM All Reduce) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  a  :  MSet\{s\}@i
3.  mset\_mon\{s\}  \mmember{}  AbMon
\mvdash{}  (a  +  0\{s\})  =  a


By

---

Latex:
((AddAllProperties  3 
THENM  ARepD  ["compound";"basic"] 
THENM  All  Reduce)  THEN  Auto)

---

Home Index