---

Step * 1 1 1 of Lemma ss-fun-fun


1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. [Z] : SeparationSpace
4. ∀G:{f:(Point(X) × Point(Y)) ⟶ Point(Z)| ss-function(X × Y;Z;f)} . ∀x:Point(X).  (λy.(G <x, y>) ∈ Point(Y ⟶ Z))
5. ∀f:Point(X × Y ⟶ Z). (λx,y. (f <x, y>) ∈ Point(X ⟶ Y ⟶ Z))
⊢ λG,x,y. (G <x, y>) ∈ Point(X × Y ⟶ Z ⟶ X ⟶ Y ⟶ Z)
BY
{ ((RWO "ss-fun-point" 0 THENA Auto) THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. X : SeparationSpace
2. Y : SeparationSpace
3. Z : SeparationSpace
4. ∀G:{f:(Point(X) × Point(Y)) ⟶ Point(Z)| ss-function(X × Y;Z;f)} . ∀x:Point(X).  (λy.(G <x, y>) ∈ Point(Y ⟶ Z))
5. ∀f:Point(X × Y ⟶ Z). (λx,y. (f <x, y>) ∈ Point(X ⟶ Y ⟶ Z))
⊢ ss-function(X × Y ⟶ Z;X ⟶ Y ⟶ Z;λG,x,y. (G <x, y>))

---

Latex:

---

Latex:

1.  [X]  :  SeparationSpace
2.  [Y]  :  SeparationSpace
3.  [Z]  :  SeparationSpace
4.  \mforall{}G:\{f:(Point(X)  \mtimes{}  Point(Y))  {}\mrightarrow{}  Point(Z)|  ss-function(X  \mtimes{}  Y;Z;f)\}  .  \mforall{}x:Point(X).
          (\mlambda{}y.(G  <x,  y>)  \mmember{}  Point(Y  {}\mrightarrow{}  Z))
5.  \mforall{}f:Point(X  \mtimes{}  Y  {}\mrightarrow{}  Z).  (\mlambda{}x,y.  (f  <x,  y>)  \mmember{}  Point(X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z))
\mvdash{}  \mlambda{}G,x,y.  (G  <x,  y>)  \mmember{}  Point(X  \mtimes{}  Y  {}\mrightarrow{}  Z  {}\mrightarrow{}  X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z)


By

---

Latex:
((RWO  "ss-fun-point"  0  THENA  Auto)  THEN  MemTypeCD  THEN  Auto)

---

Home Index