---

Step * 1 1 2 1 2 1 of Lemma path-comp-property_functionality


1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. f1 : Point(X ⟶ Y)
4. g1 : Point(Y ⟶ X)
5. ∀x:Point(X). g1(f1(x)) ≡ x
6. ∀y:Point(Y). f1(g1(y)) ≡ y
7. ∀f,g:Point(Path(X)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))
8. f : Point(Path(Y))
9. g : Point(Path(Y))
10. f@r1 ≡ g@r0
11. h : Point(Path(X))
12. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . h@t ≡ ss-comp(g1;f)@r(2) * t
13. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . h@t ≡ ss-comp(g1;g)@(r(2) * t) - r1
14. t : {x:ℝ| x ∈ [(r1/r(2)), r1]} 
15. h@t ≡ ss-comp(g1;g)@(r(2) * t) - r1
16. (r(2) * t) - r1 ∈ {t:ℝ| (r0 ≤ t) ∧ (t ≤ r1)} 
17. t ∈ {t:ℝ| (r0 ≤ t) ∧ (t ≤ r1)} 
⊢ ss-comp(f1;h)@t ≡ g@(r(2) * t) - r1
BY
{ ((Subst' ss-comp(g1;g)@(r(2) * t) - r1 ~ g1(g@(r(2) * t) - r1) -3 THENA RepeatFor 2 ((Computation THEN Auto)))
   THEN (Subst' ss-comp(f1;h)@t ~ f1(h@t) 0 THENA RepeatFor 2 ((Computation THEN Auto)))
   ) }

1
1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. f1 : Point(X ⟶ Y)
4. g1 : Point(Y ⟶ X)
5. ∀x:Point(X). g1(f1(x)) ≡ x
6. ∀y:Point(Y). f1(g1(y)) ≡ y
7. ∀f,g:Point(Path(X)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))
8. f : Point(Path(Y))
9. g : Point(Path(Y))
10. f@r1 ≡ g@r0
11. h : Point(Path(X))
12. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . h@t ≡ ss-comp(g1;f)@r(2) * t
13. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . h@t ≡ ss-comp(g1;g)@(r(2) * t) - r1
14. t : {x:ℝ| x ∈ [(r1/r(2)), r1]} 
15. h@t ≡ g1(g@(r(2) * t) - r1)
16. (r(2) * t) - r1 ∈ {t:ℝ| (r0 ≤ t) ∧ (t ≤ r1)} 
17. t ∈ {t:ℝ| (r0 ≤ t) ∧ (t ≤ r1)} 
⊢ f1(h@t) ≡ g@(r(2) * t) - r1

---

Latex:

---

Latex:

1.  [X]  :  SeparationSpace
2.  [Y]  :  SeparationSpace
3.  f1  :  Point(X  {}\mrightarrow{}  Y)
4.  g1  :  Point(Y  {}\mrightarrow{}  X)
5.  \mforall{}x:Point(X).  g1(f1(x))  \mequiv{}  x
6.  \mforall{}y:Point(Y).  f1(g1(y))  \mequiv{}  y
7.  \mforall{}f,g:Point(Path(X)).    (f@r1  \mequiv{}  g@r0  {}\mRightarrow{}  (\mexists{}h:Point(Path(X)).  path-comp-rel(X;f;g;h)))
8.  f  :  Point(Path(Y))
9.  g  :  Point(Path(Y))
10.  f@r1  \mequiv{}  g@r0
11.  h  :  Point(Path(X))
12.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  h@t  \mequiv{}  ss-comp(g1;f)@r(2)  *  t
13.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  h@t  \mequiv{}  ss-comp(g1;g)@(r(2)  *  t)  -  r1
14.  t  :  \{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\} 
15.  h@t  \mequiv{}  ss-comp(g1;g)@(r(2)  *  t)  -  r1
16.  (r(2)  *  t)  -  r1  \mmember{}  \{t:\mBbbR{}|  (r0  \mleq{}  t)  \mwedge{}  (t  \mleq{}  r1)\} 
17.  t  \mmember{}  \{t:\mBbbR{}|  (r0  \mleq{}  t)  \mwedge{}  (t  \mleq{}  r1)\} 
\mvdash{}  ss-comp(f1;h)@t  \mequiv{}  g@(r(2)  *  t)  -  r1


By

---

Latex:
((Subst'  ss-comp(g1;g)@(r(2)  *  t)  -  r1  \msim{}  g1(g@(r(2)  *  t)  -  r1)  -3
    THENA  RepeatFor  2  ((Computation  THEN  Auto))
    )
  THEN  (Subst'  ss-comp(f1;h)@t  \msim{}  f1(h@t)  0  THENA  RepeatFor  2  ((Computation  THEN  Auto)))
  )

---

Home Index