---

Step * of Lemma gen-divisors-sum_wf

∀[r:CRng]. ∀[n:ℕ+]. ∀[f:ℕ+n + 1 ⟶ |r|].  (Σ i|n. f[i] ∈ |r|)
BY
{ xxx(Auto THEN Unfold `gen-divisors-sum` 0 THEN (Assert [1, n + 1) ∈ bag(ℕ+n + 1) BY Auto) THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[f:\mBbbN{}\msupplus{}n  +  1  {}\mrightarrow{}  |r|].    (\mSigma{}  i|n.  f[i]  \mmember{}  |r|)


By

---

Latex:
xxx(Auto
        THEN  Unfold  `gen-divisors-sum`  0
        THEN  (Assert  [1,  n  +  1)  \mmember{}  bag(\mBbbN{}\msupplus{}n  +  1)  BY
                                Auto)
        THEN  Auto)xxx

---

Home Index