---

Step * of Lemma fset-image-compose

∀[T,A,B:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[eqb:EqDecider(B)]. ∀[f:T ⟶ A]. ∀[g:A ⟶ B]. ∀[s:fset(T)].
  (g"(f"(s)) = g o f"(s) ∈ fset(B))
BY
{ (Auto
   THEN (FsetExt THEN SupposeNot THEN Assert ⌜False⌝⋅ THEN Auto)
   THEN (All (RWW "member-fset-image-iff") THENA Auto)
   THEN SqExRepD
   THEN D -1
   THEN D 0
   THEN All (RepUR ``compose``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,A,B:Type].  \mforall{}[eqt:EqDecider(T)].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[eqb:EqDecider(B)].  \mforall{}[f:T  {}\mrightarrow{}  A].
\mforall{}[g:A  {}\mrightarrow{}  B].  \mforall{}[s:fset(T)].
    (g"(f"(s))  =  g  o  f"(s))


By

---

Latex:
(Auto
  THEN  (FsetExt  THEN  SupposeNot  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (All  (RWW  "member-fset-image-iff")  THENA  Auto)
  THEN  SqExRepD
  THEN  D  -1
  THEN  D  0
  THEN  All  (RepUR  ``compose``)
  THEN  Auto)

---

Home Index