---

Step * of Lemma rng_lsum_functionality_wrt_permutation

∀[r:Rng]. ∀[A:Type]. ∀[f:A ⟶ |r|]. ∀[as,bs:A List].
  Σ{r} x ∈ as. f[x] = Σ{r} x ∈ bs. f[x] ∈ |r| supposing permutation(A;as;bs)
BY
{ (Auto
   THEN Unfold `rng_lsum` 0
   THEN BLemma `reduce-permutation`
   THEN Auto
   THEN Try ((RepUR ``so_apply`` 0 THEN D 0 THEN Reduce 0 THEN Auto THEN Fold `infix_ap` 0 THEN Auto))) }

1
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))

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  |r|].  \mforall{}[as,bs:A  List].
    \mSigma{}\{r\}  x  \mmember{}  as.  f[x]  =  \mSigma{}\{r\}  x  \mmember{}  bs.  f[x]  supposing  permutation(A;as;bs)


By

---

Latex:
...

---

Home Index