---

Step * of Lemma fset_of_mset_mem

∀s:DSet. ∀a:MSet{s}. ∀c:|s|.  c ∈b fset_of_mset(s;a) = c ∈b a
BY
{ ((RepD THENM OnVar `a' MoveToConcl 
THENM BLemma `mset_ind_a`) THENA Auto) }

1
1. s : DSet
2. c : |s|
⊢ ∀w:MSet{s}. SqStable(c ∈b fset_of_mset(s;w) = c ∈b w)

2
1. s : DSet
2. c : |s|
⊢ c ∈b fset_of_mset(s;0{s}) = c ∈b 0{s}

3
1. s : DSet
2. c : |s|
⊢ ∀x:|s|. c ∈b fset_of_mset(s;mset_inj{s}(x)) = c ∈b mset_inj{s}(x)

4
1. s : DSet
2. c : |s|
⊢ ∀ys,ys':MSet{s}.
    (c ∈b fset_of_mset(s;ys) = c ∈b ys
    ⇒ c ∈b fset_of_mset(s;ys') = c ∈b ys'
    ⇒ c ∈b fset_of_mset(s;ys + ys') = c ∈b ys + ys')

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:MSet\{s\}.  \mforall{}c:|s|.    c  \mmember{}\msubb{}  fset\_of\_mset(s;a)  =  c  \mmember{}\msubb{}  a


By

---

Latex:
((RepD  THENM  OnVar  `a'  MoveToConcl 
THENM  BLemma  `mset\_ind\_a`)  THENA  Auto)

---

Home Index