---

Step * of Lemma map_functionality_2

∀A,B:Type. ∀as:A List. ∀f,f':A ⟶ B. ∀as:A List.
  ((f = f' ∈ ({x:A| mem_f(A;x;as)}  ⟶ B)) ⇒ (map(f;as) = map(f';as) ∈ (B List)))
BY
{ Auto }

1
1. A : Type
2. B : Type
3. as : A List
4. f : A ⟶ B
5. f' : A ⟶ B
6. a1 : A List
7. f = f' ∈ ({x:A| mem_f(A;x;a1)}  ⟶ B)
⊢ map(f;a1) = map(f';a1) ∈ (B List)

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}as:A  List.  \mforall{}f,f':A  {}\mrightarrow{}  B.  \mforall{}as:A  List.    ((f  =  f')  {}\mRightarrow{}  (map(f;as)  =  map(f';as)))


By

---

Latex:
Auto

---

Home Index