---

Step * of Lemma basic-formal-sum-strong-subtype

∀[K:RngSig]. ∀[S,T:Type].  strong-subtype(basic-formal-sum(K;S);basic-formal-sum(K;T)) supposing strong-subtype(S;T)
BY
{ (Unfold `basic-formal-sum` 0 THEN EAuto 1) }

---

Latex:

---

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


By

---

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

---

Home Index