---

Step * of Lemma cube-set-restriction-comp

∀X:CubicalSet. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I).  (g(f(a)) = (f o g)(a) ∈ X(K))
BY
{ (Auto
   THEN (Assert X ∈ CubicalSet BY
               Trivial)
   THEN RepeatFor 2 (D 1)
   THEN RepUR ``cube-set-restriction`` 0
   THEN All Reduce
   THEN Auto
   THEN RWO "3" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}a:X(I).
    (g(f(a))  =  (f  o  g)(a))


By

---

Latex:
(Auto
  THEN  (Assert  X  \mmember{}  CubicalSet  BY
                          Trivial)
  THEN  RepeatFor  2  (D  1)
  THEN  RepUR  ``cube-set-restriction``  0
  THEN  All  Reduce
  THEN  Auto
  THEN  RWO  "3"  0
  THEN  Auto)

---

Home Index