---

Step * of Lemma singlevalued-graph_functionality

∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
  ⇒ (∀g1,g2:coSet{i:l}.  (seteq(g1;g2) ⇒ (singlevalued-graph(A;a.B[a];g1) ⇐⇒ singlevalued-graph(A;a.B[a];g2)))))
BY
{ (Auto
   THEN (All (RWO "singlevalued-graph-iff") THENA Auto)
   THEN RepeatFor 8 ((ParallelLast' THENA (Auto THEN ((RWO "6" (-1) THEN Auto) ORELSE (RWO "6" 0 THEN Auto)))))) }

---

Latex:

---

Latex:
\mforall{}A:coSet\{i:l\}.  \mforall{}B:\{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}.
    ((\mforall{}a1,a2:coSet\{i:l\}.    ((a1  \mmember{}  A)  {}\mRightarrow{}  (a2  \mmember{}  A)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  seteq(B[a1];B[a2])))
    {}\mRightarrow{}  (\mforall{}g1,g2:coSet\{i:l\}.
                (seteq(g1;g2)  {}\mRightarrow{}  (singlevalued-graph(A;a.B[a];g1)  \mLeftarrow{}{}\mRightarrow{}  singlevalued-graph(A;a.B[a];g2)))))


By

---

Latex:
(Auto
  THEN  (All  (RWO  "singlevalued-graph-iff")  THENA  Auto)
  THEN  RepeatFor  8  ((ParallelLast'
                                        THENA  (Auto  THEN  ((RWO  "6"  (-1)  THEN  Auto)  ORELSE  (RWO  "6"  0  THEN  Auto)))
                                        )))

---

Home Index