---

Step * of Lemma nh-comp-nc-m

∀[I,K:fset(ℕ)]. ∀[i,j:ℕ]. ∀[f:K ⟶ I+j].  (m(i;j) ⋅ f i) = f i ∧ f j ∈ Point(dM(K)) supposing i ∈ I
BY
{ (Auto
   THEN (Assert i ∈ names(I+j) BY
               (MemTypeCD THEN EAuto 1))
   THEN (Assert j ∈ names(I+j) BY
               (MemTypeCD THEN EAuto 1))
   THEN (RWO "nh-comp-sq" 0 THENA Auto)
   THEN RepUR ``nc-m compose`` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[I,K:fset(\mBbbN{})].  \mforall{}[i,j:\mBbbN{}].  \mforall{}[f:K  {}\mrightarrow{}  I+j].    (m(i;j)  \mcdot{}  f  i)  =  f  i  \mwedge{}  f  j  supposing  i  \mmember{}  I


By

---

Latex:
(Auto
  THEN  (Assert  i  \mmember{}  names(I+j)  BY
                          (MemTypeCD  THEN  EAuto  1))
  THEN  (Assert  j  \mmember{}  names(I+j)  BY
                          (MemTypeCD  THEN  EAuto  1))
  THEN  (RWO  "nh-comp-sq"  0  THENA  Auto)
  THEN  RepUR  ``nc-m  compose``  0
  THEN  AutoSplit)

---

Home Index