---

Step * of Lemma l_sum_permute

∀[L1,L2:ℤ List].  l_sum(L1) = l_sum(L2) ∈ ℤ supposing permutation(ℤ;L1;L2)
BY
{ (Auto THEN Unfold `l_sum` 0 THEN BLemma `reduce-permutation` THEN Auto THEN D 0 THEN RepUR ``so_apply`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L1,L2:\mBbbZ{}  List].    l\_sum(L1)  =  l\_sum(L2)  supposing  permutation(\mBbbZ{};L1;L2)


By

---

Latex:
(Auto
  THEN  Unfold  `l\_sum`  0
  THEN  BLemma  `reduce-permutation`
  THEN  Auto
  THEN  D  0
  THEN  RepUR  ``so\_apply``  0
  THEN  Auto)

---

Home Index