---

Step * of Lemma null-formal-sum-mul

∀[S:Type]. ∀K:CRng. ∀[x:basic-formal-sum(K;S)]. ∀k:|K|. (null-formal-sum(K;S;x) ⇒ null-formal-sum(K;S;k * x))
BY
{ (Auto THEN ParallelLast THEN ExRepD THEN (D 0 With ⌜k * b⌝  THEN Auto) THEN D 0 With ⌜ss⌝  THEN Auto) }

1
1. S : Type
2. K : CRng
3. x : basic-formal-sum(K;S)
4. k : |K|
5. b : bag(|K| × S)
6. ss : bag(S)
7. x = ((b + -(b)) + 0 * ss) ∈ bag(|K| × S)
⊢ k * x = ((k * b + -(k * b)) + 0 * ss) ∈ bag(|K| × S)

---

Latex:

---

Latex:
\mforall{}[S:Type]
    \mforall{}K:CRng
        \mforall{}[x:basic-formal-sum(K;S)].  \mforall{}k:|K|.  (null-formal-sum(K;S;x)  {}\mRightarrow{}  null-formal-sum(K;S;k  *  x))


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}k  *  b\mkleeneclose{}    THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}ss\mkleeneclose{} 
  THEN  Auto)

---

Home Index