---

Step * of Lemma rng_lsum_swap

∀[r:Rng]. ∀[A,B:Type]. ∀[F:A ⟶ B ⟶ |r|]. ∀[as:A List]. ∀[bs:B List].
  (Σ{r} a ∈ as. Σ{r} b ∈ bs. F[a;b] = Σ{r} b ∈ bs. Σ{r} a ∈ as. F[a;b] ∈ |r|)
BY
{ (RepeatFor 2 (InductionOnList)
   THEN Reduce 0
   THEN Auto
   THEN Try ((RWO "rng_lsum_0" 0 THEN Auto))
   THEN (RWW "rng_lsum_plus 7" 0 THENA Auto)
   THEN RW RngNormC 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[A,B:Type].  \mforall{}[F:A  {}\mrightarrow{}  B  {}\mrightarrow{}  |r|].  \mforall{}[as:A  List].  \mforall{}[bs:B  List].
    (\mSigma{}\{r\}  a  \mmember{}  as.  \mSigma{}\{r\}  b  \mmember{}  bs.  F[a;b]  =  \mSigma{}\{r\}  b  \mmember{}  bs.  \mSigma{}\{r\}  a  \mmember{}  as.  F[a;b])


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((RWO  "rng\_lsum\_0"  0  THEN  Auto))
  THEN  (RWW  "rng\_lsum\_plus  7"  0  THENA  Auto)
  THEN  RW  RngNormC  0
  THEN  Auto)

---

Home Index