---

Step * of Lemma fl-morph-comp2

∀[I,J,K:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[g:K ⟶ J]. ∀[x:Point(face_lattice(I))].
  (((x)<f>)<g> = (x)<f ⋅ g> ∈ Point(face_lattice(K)))
BY
{ (InstLemma `fl-morph-comp` []
   THEN RepeatFor 5 (ParallelLast')
   THEN Auto
   THEN (ApFunToHypEquands `Z' ⌜Z x⌝  ⌜Point(face_lattice(K))⌝ (-2)⋅ THENA Auto)
   THEN RepUR ``compose`` -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J,K:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[g:K  {}\mrightarrow{}  J].  \mforall{}[x:Point(face\_lattice(I))].    (((x)<f>)<g>  =  (x)<f  \mcdot{}  g>)


By

---

Latex:
(InstLemma  `fl-morph-comp`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  Auto
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x\mkleeneclose{}    \mkleeneopen{}Point(face\_lattice(K))\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``compose``  -1
  THEN  Auto)

---

Home Index