---

Step * of Lemma only-bag-map

∀[f:Top]. ∀[T:Type]. ∀[b:bag(T)].  only(bag-map(f;b)) ~ f only(b) supposing #(b) = 1 ∈ ℤ
BY
{ (Auto THEN ElimBagSizeOne) }

1
1. f : Top
2. T : Type
3. b : bag(T)
4. #(b) = 1 ∈ ℤ
5. b ~ {only(b)}
6. x : T
⊢ only(bag-map(f;{x})) ~ f only({x})

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[T:Type].  \mforall{}[b:bag(T)].    only(bag-map(f;b))  \msim{}  f  only(b)  supposing  \#(b)  =  1


By

---

Latex:
(Auto  THEN  ElimBagSizeOne)

---

Home Index