---

Step * of Lemma formal-sum-mul-1

∀[S:Type]. ∀[K:Rng]. ∀[x:formal-sum(K;S)].  (1 * x = x ∈ formal-sum(K;S))
BY
{ (RepeatFor 2 (Intro)
   THEN (Assert ∀[x:basic-formal-sum(K;S)]. (1 * x = x ∈ basic-formal-sum(K;S)) BY
               (RepUR ``basic-formal-sum formal-sum-mul`` 0 THEN Auto))
   ) }

1
1. S : Type
2. K : Rng
3. x : bag(|K| × S)
⊢ bag-map(λp.let k',s = p in <1 * k', s>;x) = x ∈ bag(|K| × S)

2
1. [S] : Type
2. [K] : Rng
3. ∀[x:basic-formal-sum(K;S)]. (1 * x = x ∈ basic-formal-sum(K;S))
⊢ ∀[x:formal-sum(K;S)]. (1 * x = x ∈ formal-sum(K;S))

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:Rng].  \mforall{}[x:formal-sum(K;S)].    (1  *  x  =  x)


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (Assert  \mforall{}[x:basic-formal-sum(K;S)].  (1  *  x  =  x)  BY
                          (RepUR  ``basic-formal-sum  formal-sum-mul``  0  THEN  Auto))
  )

---

Home Index