---

Step * 1 2 of Lemma map_permr_func


1. A : Type
2. B : Type
3. f : A ⟶ B
4. as : A List
5. as' : A List
6. ||as|| = ||as'|| ∈ ℤ
7. ∃p:Sym(||as||). ∀i:ℕ||as||. (as[p.f i] = as'[i] ∈ A)
8. ||map(f;as)|| = ||map(f;as')|| ∈ ℤ
⊢ ∃p:Sym(||map(f;as)||). ∀i:ℕ||map(f;as)||. (map(f;as)[p.f i] = map(f;as')[i] ∈ B)
BY
{ (((D 7 THEN With p (D 0)) THENM D 0) THENA Auto') }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. as : A List
5. as' : A List
6. ||as|| = ||as'|| ∈ ℤ
7. p : Sym(||as||)
8. ∀i:ℕ||as||. (as[p.f i] = as'[i] ∈ A)
9. ||map(f;as)|| = ||map(f;as')|| ∈ ℤ
10. i : ℕ||map(f;as)||
⊢ map(f;as)[p.f i] = map(f;as')[i] ∈ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  as  :  A  List
5.  as'  :  A  List
6.  ||as||  =  ||as'||
7.  \mexists{}p:Sym(||as||).  \mforall{}i:\mBbbN{}||as||.  (as[p.f  i]  =  as'[i])
8.  ||map(f;as)||  =  ||map(f;as')||
\mvdash{}  \mexists{}p:Sym(||map(f;as)||).  \mforall{}i:\mBbbN{}||map(f;as)||.  (map(f;as)[p.f  i]  =  map(f;as')[i])


By

---

Latex:
(((D  7  THEN  With  p  (D  0))  THENM  D  0)  THENA  Auto')

---

Home Index