---

Step * of Lemma basic-formal-sum-subtype

∀[K:RngSig]. ∀[S,T:Type].  basic-formal-sum(K;S) ⊆r basic-formal-sum(K;T) supposing S ⊆r T
BY
{ (Unfold `basic-formal-sum` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K:RngSig].  \mforall{}[S,T:Type].    basic-formal-sum(K;S)  \msubseteq{}r  basic-formal-sum(K;T)  supposing  S  \msubseteq{}r  T


By

---

Latex:
(Unfold  `basic-formal-sum`  0  THEN  Auto)

---

Home Index