---

Step * of Lemma fset-image-add

∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[x:T]. ∀[s:fset(T)].
  (f"(fset-add(eqt;x;s)) = {f x} ⋃ f"(s) ∈ fset(A))
BY
{ (Auto
   THEN (Subst' {f x} = f"({x}) ∈ fset(A) 0 THENA Auto)
   THEN ((RWO  "fset-image-union<" 0 THENA Auto) THEN EqCD)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[eqt:EqDecider(T)].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[f:T  {}\mrightarrow{}  A].  \mforall{}[x:T].  \mforall{}[s:fset(T)].
    (f"(fset-add(eqt;x;s))  =  \{f  x\}  \mcup{}  f"(s))


By

---

Latex:
(Auto
  THEN  (Subst'  \{f  x\}  =  f"(\{x\})  0  THENA  Auto)
  THEN  ((RWO    "fset-image-union<"  0  THENA  Auto)  THEN  EqCD)
  THEN  Auto)

---

Home Index