---

Step * 1 1 1 1 1 1 1 1 of Lemma sub-free-dim-1


1. K : CRng
2. S : Type
3. a : S
⊢ (∀p:|K| × S. (p ↓∈ [] ⇒ ((snd(p)) = a ∈ S))) ⇒ ([] = {<Σ(p∈[]). fst(p), a>} ∈ formal-sum(K;S))
BY
{ (Auto THEN (Subst' Σ(p∈[]). fst(p) ~ 0 0 THENA Computation)) }

1
1. K : CRng
2. S : Type
3. a : S
4. ∀p:|K| × S. (p ↓∈ [] ⇒ ((snd(p)) = a ∈ S))
⊢ [] = {<0, a>} ∈ formal-sum(K;S)

---

Latex:

---

Latex:

1.  K  :  CRng
2.  S  :  Type
3.  a  :  S
\mvdash{}  (\mforall{}p:|K|  \mtimes{}  S.  (p  \mdownarrow{}\mmember{}  []  {}\mRightarrow{}  ((snd(p))  =  a)))  {}\mRightarrow{}  ([]  =  \{<\mSigma{}(p\mmember{}[]).  fst(p),  a>\})


By

---

Latex:
(Auto  THEN  (Subst'  \mSigma{}(p\mmember{}[]).  fst(p)  \msim{}  0  0  THENA  Computation))

---

Home Index