---

Step * of Lemma pscm-equal2

No Annotations
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)]. ∀[f,g:psc_map{j:l}(C; A; B)].
  f = g ∈ psc_map{j:l}(C; A; B) supposing ∀K:cat-ob(C). ∀x:A(K).  ((f K x) = (g K x) ∈ B(K))
BY
{ (Auto THEN BLemma `pscm-equal` THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[A,B:ps\_context\{j:l\}(C)].  \mforall{}[f,g:psc\_map\{j:l\}(C;  A;  B)].
    f  =  g  supposing  \mforall{}K:cat-ob(C).  \mforall{}x:A(K).    ((f  K  x)  =  (g  K  x))


By

---

Latex:
(Auto  THEN  BLemma  `pscm-equal`  THEN  Auto)

---

Home Index