---

Step * of Lemma single-valued-bag-map

∀[A,B:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ B].  single-valued-bag(bag-map(f;as);B) supposing single-valued-bag(as;A)
BY
{ (Auto
   THEN All (Unfold `single-valued-bag`)
   THEN Auto
   THEN BagMemberD (-2)
   THEN BagMemberD (-1)
   THEN SquashExRepD
   THEN InstHyp [⌜v1⌝;⌜v⌝] (-9)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[as:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  B].
    single-valued-bag(bag-map(f;as);B)  supposing  single-valued-bag(as;A)


By

---

Latex:
(Auto
  THEN  All  (Unfold  `single-valued-bag`)
  THEN  Auto
  THEN  BagMemberD  (-2)
  THEN  BagMemberD  (-1)
  THEN  SquashExRepD
  THEN  InstHyp  [\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]  (-9)\mcdot{}
  THEN  Auto)

---

Home Index