Step * of Lemma mset_sum_ident_r

s:DSet. ∀a:MSet{s}.  ((a 0{s}) a ∈ MSet{s})
BY
((RepD THENM Assert mset_mon{s} ∈ AbMon) THENA Auto) }

1
1. DSet@i'
2. MSet{s}@i
3. mset_mon{s} ∈ AbMon
⊢ (a 0{s}) a ∈ MSet{s}


Latex:


Latex:
\mforall{}s:DSet.  \mforall{}a:MSet\{s\}.    ((a  +  0\{s\})  =  a)


By


Latex:
((RepD  THENM  Assert  mset\_mon\{s\}  \mmember{}  AbMon)  THENA  Auto)




Home Index