---

Step * of Lemma compose-dma-hom

∀[dma1,dma2,dma3:DeMorganAlgebra]. ∀[f:dma-hom(dma1;dma2)]. ∀[g:dma-hom(dma2;dma3)].  (g o f ∈ dma-hom(dma1;dma3))
BY
{ (Auto THEN D -2 THEN D -1 THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. dma1 : DeMorganAlgebra
2. dma2 : DeMorganAlgebra
3. dma3 : DeMorganAlgebra
4. f : Hom(dma1;dma2)
5. ∀[a:Point(dma1)]. (¬(f a) = (f ¬(a)) ∈ Point(dma2))
6. g : Hom(dma2;dma3)
7. ∀[a:Point(dma2)]. (¬(g a) = (g ¬(a)) ∈ Point(dma3))
⊢ g o f ∈ Hom(dma1;dma3)

---

Latex:

---

Latex:
\mforall{}[dma1,dma2,dma3:DeMorganAlgebra].  \mforall{}[f:dma-hom(dma1;dma2)].  \mforall{}[g:dma-hom(dma2;dma3)].
    (g  o  f  \mmember{}  dma-hom(dma1;dma3))


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index