---

Step * 1 of Lemma rng_lsum_functionality_wrt_permutation


1. r : Rng
2. A : Type
3. f : A ⟶ |r|
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
⊢ permutation(|r|;map(λx.f[x];as);map(λx.f[x];bs))
BY
{ EAuto 1 }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  A  :  Type
3.  f  :  A  {}\mrightarrow{}  |r|
4.  as  :  A  List
5.  bs  :  A  List
6.  permutation(A;as;bs)
\mvdash{}  permutation(|r|;map(\mlambda{}x.f[x];as);map(\mlambda{}x.f[x];bs))


By

---

Latex:
EAuto  1

---

Home Index