---

Step * of Lemma free-vs-dim-1-ext

∀S:Type. (S ⇒ (∀K:CRng. free-vs(K;S) ≅ one-dim-vs(K) supposing ∀x,y:S.  (x = y ∈ S)))
BY
{ Extract of Obid: free-vs-dim-1
  not unfolding  bag-summation rng_one rng_zero rng_plus rng_times
  finishing with (Auto THEN Computation)
  normalizes to:
  
  λS,s,K. <λx.Σ(p∈x). let k,s = p in k * 1, λk.{<* k 1, s>}, λb.Ax, λa.Ax> }

---

Latex:

---

Latex:
\mforall{}S:Type.  (S  {}\mRightarrow{}  (\mforall{}K:CRng.  free-vs(K;S)  \mcong{}  one-dim-vs(K)  supposing  \mforall{}x,y:S.    (x  =  y)))


By

---

Latex:
Extract  of  Obid:  free-vs-dim-1
not  unfolding    bag-summation  rng\_one  rng\_zero  rng\_plus  rng\_times
finishing  with  (Auto  THEN  Computation)
normalizes  to:

\mlambda{}S,s,K.  <\mlambda{}x.\mSigma{}(p\mmember{}x).  let  k,s  =  p  in  k  *  1,  \mlambda{}k.\{<*  k  1,  s>\},  \mlambda{}b.Ax,  \mlambda{}a.Ax>

---

Home Index