---

Step * of Lemma rng_mssum_swap

∀r:Rng. ∀s,s':DSet. ∀f:|s| ⟶ |s'| ⟶ |r|. ∀a:MSet{s}. ∀b:MSet{s'}.
  ((Σx ∈ a. Σy ∈ b. f[x;y]) = (Σy ∈ b. Σx ∈ a. f[x;y]) ∈ |r|)
BY
{ ProveSpecializedLemma `mset_for_swap` 1 [parm{i};r↓+gp] (FoldsC ``rng_when rng_mssum`` ANDTHENC AbReduceC) }

---

Latex:

---

Latex:
\mforall{}r:Rng.  \mforall{}s,s':DSet.  \mforall{}f:|s|  {}\mrightarrow{}  |s'|  {}\mrightarrow{}  |r|.  \mforall{}a:MSet\{s\}.  \mforall{}b:MSet\{s'\}.
    ((\mSigma{}x  \mmember{}  a.  \mSigma{}y  \mmember{}  b.  f[x;y])  =  (\mSigma{}y  \mmember{}  b.  \mSigma{}x  \mmember{}  a.  f[x;y]))


By

---

Latex:
ProveSpecializedLemma  `mset\_for\_swap`  1  [parm\{i\};r\mdownarrow{}+gp
]  (FoldsC  ``rng\_when  rng\_mssum``  ANDTHENC  AbReduceC)

---

Home Index