---

Step * of Lemma formal-sum-mul-mul

∀[S:Type]. ∀[K:CRng]. ∀[k,b:|K|]. ∀[x:formal-sum(K;S)].  (k * b * x = k * b * x ∈ formal-sum(K;S))
BY
{ (RepeatFor 4 (Intro)
   THEN (Assert ∀[x:basic-formal-sum(K;S)]. (k * b * x = k * b * x ∈ basic-formal-sum(K;S)) BY
               (RepUR ``basic-formal-sum formal-sum-mul`` 0
                THEN Auto
                THEN (RWO  "bag-map-map" 0 THENM RepUR ``compose`` 0)
                THEN Auto))
   ) }

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

2
1. [S] : Type
2. [K] : CRng
3. [k] : |K|
4. [b] : |K|
5. ∀[x:basic-formal-sum(K;S)]. (k * b * x = k * b * x ∈ basic-formal-sum(K;S))
⊢ ∀[x:formal-sum(K;S)]. (k * b * x = k * b * x ∈ formal-sum(K;S))

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:CRng].  \mforall{}[k,b:|K|].  \mforall{}[x:formal-sum(K;S)].    (k  *  b  *  x  =  k  *  b  *  x)


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  (Assert  \mforall{}[x:basic-formal-sum(K;S)].  (k  *  b  *  x  =  k  *  b  *  x)  BY
                          (RepUR  ``basic-formal-sum  formal-sum-mul``  0
                            THEN  Auto
                            THEN  (RWO    "bag-map-map"  0  THENM  RepUR  ``compose``  0)
                            THEN  Auto))
  )

---

Home Index