---

Step * of Lemma Q-R-pre-preserving-compose

∀es:EO
  ∀[P1,P2:E ⟶ ℙ]. ∀[Q1,Q2,Q3:E ⟶ E ⟶ ℙ].
    ∀f1:{e:E| P1 e}  ⟶ {e:E| P2 e} . ∀f2:{e:E| P2 e}  ⟶ E.
      (f1 is Q2-Q3-pre-preserving on P1 ⇒ f2 is Q1-Q2-pre-preserving on P2 ⇒ f2 o f1 is Q1-Q3-pre-preserving on P1)
BY
{ (All (Unfolds ``Q-R-pre-preserving compose``) THEN All Reduce THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}es:EO
    \mforall{}[P1,P2:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q1,Q2,Q3:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f1:\{e:E|  P1  e\}    {}\mrightarrow{}  \{e:E|  P2  e\}  .  \mforall{}f2:\{e:E|  P2  e\}    {}\mrightarrow{}  E.
            (f1  is  Q2-Q3-pre-preserving  on  P1
            {}\mRightarrow{}  f2  is  Q1-Q2-pre-preserving  on  P2
            {}\mRightarrow{}  f2  o  f1  is  Q1-Q3-pre-preserving  on  P1)


By

---

Latex:
(All  (Unfolds  ``Q-R-pre-preserving  compose``)  THEN  All  Reduce  THEN  Auto)\mcdot{}

---

Home Index