---

Step * 1 1 of Lemma ss-fun-fun

.....assertion..... 
1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. [Z] : SeparationSpace
4. λF,p. (F (fst(p)) (snd(p))) ∈ Point(X ⟶ Y ⟶ Z ⟶ X × Y ⟶ Z)
⊢ λG,x,y. (G <x, y>) ∈ Point(X × Y ⟶ Z ⟶ X ⟶ Y ⟶ Z)
BY
{ (Thin (-1)
   THEN (Assert ∀G:{f:(Point(X) × Point(Y)) ⟶ Point(Z)| ss-function(X × Y;Z;f)} . ∀x:Point(X).
                  (λy.(G <x, y>) ∈ Point(Y ⟶ Z)) BY
               ((RWW "ss-fun-point" 0 THEN Auto)
                THEN DVar `G'
                THEN MemTypeCD
                THEN Auto
                THEN D 0
                THEN Auto
                THEN Reduce 0
                THEN All (RepUR ``ss-function``)
                THEN BackThruSomeHyp
                THEN ParallelLast
                THEN (RWO "prod-ss-sep" 0 THENA Auto)
                THEN Reduce 0
                THEN ParallelLast
                THEN Auto
                THEN (D -1 THEN Auto)
                THEN (Assert ⌜False⌝⋅ THEN Auto)
                THEN MoveToConcl (-1)
                THEN Fold `not` 0
                THEN Fold `ss-eq` 0
                THEN Auto))
   THEN (Assert ∀f:Point(X × Y ⟶ Z). (λx,y. (f <x, y>) ∈ Point(X ⟶ Y ⟶ Z)) BY
               (Auto
                THEN RWO "ss-fun-point" 0
                THEN Auto
                THEN MemTypeCD
                THEN Auto
                THEN (RWO "ss-fun-point prod-ss-point" (-1) THENA Auto)
                THEN D -1
                THEN (D 0 THEN Reduce 0)
                THEN Auto
                THEN RWO "ss-fun-eq" 0
                THEN Auto
                THEN RepUR ``ss-ap`` 0
                THEN BackThruSomeHyp'
                THEN ParallelOp -2
                THEN (RWO "prod-ss-sep" 0 THENA Auto)
                THEN Reduce 0
                THEN ParallelOp -2
                THEN (D -1 THEN Auto)
                THEN (Assert ⌜False⌝⋅ THEN Auto)
                THEN MoveToConcl (-1)
                THEN Fold `not` 0
                THEN Fold `ss-eq` 0
                THEN Auto))) }

1
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)

---

Latex:

---

Latex:
.....assertion..... 
1.  [X]  :  SeparationSpace
2.  [Y]  :  SeparationSpace
3.  [Z]  :  SeparationSpace
4.  \mlambda{}F,p.  (F  (fst(p))  (snd(p)))  \mmember{}  Point(X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z  {}\mrightarrow{}  X  \mtimes{}  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:
(Thin  (-1)
  THEN  (Assert  \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))  BY
                          ((RWW  "ss-fun-point"  0  THEN  Auto)
                            THEN  DVar  `G'
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  D  0
                            THEN  Auto
                            THEN  Reduce  0
                            THEN  All  (RepUR  ``ss-function``)
                            THEN  BackThruSomeHyp
                            THEN  ParallelLast
                            THEN  (RWO  "prod-ss-sep"  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  ParallelLast
                            THEN  Auto
                            THEN  (D  -1  THEN  Auto)
                            THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
                            THEN  MoveToConcl  (-1)
                            THEN  Fold  `not`  0
                            THEN  Fold  `ss-eq`  0
                            THEN  Auto))
  THEN  (Assert  \mforall{}f:Point(X  \mtimes{}  Y  {}\mrightarrow{}  Z).  (\mlambda{}x,y.  (f  <x,  y>)  \mmember{}  Point(X  {}\mrightarrow{}  Y  {}\mrightarrow{}  Z))  BY
                          (Auto
                            THEN  RWO  "ss-fun-point"  0
                            THEN  Auto
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  (RWO  "ss-fun-point  prod-ss-point"  (-1)  THENA  Auto)
                            THEN  D  -1
                            THEN  (D  0  THEN  Reduce  0)
                            THEN  Auto
                            THEN  RWO  "ss-fun-eq"  0
                            THEN  Auto
                            THEN  RepUR  ``ss-ap``  0
                            THEN  BackThruSomeHyp'
                            THEN  ParallelOp  -2
                            THEN  (RWO  "prod-ss-sep"  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  ParallelOp  -2
                            THEN  (D  -1  THEN  Auto)
                            THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
                            THEN  MoveToConcl  (-1)
                            THEN  Fold  `not`  0
                            THEN  Fold  `ss-eq`  0
                            THEN  Auto)))

---

Home Index