---

Step * 1 of Lemma mfun-subtype2

.....set predicate..... 
1. X : Type
2. Y : Type
3. d : metric(X)
4. d' : metric(Y)
5. A : Type
6. A ⊆r X
7. x : X ⟶ Y
8. x:FUN(X;Y)
⊢ x:FUN(A;Y)
BY
{ RepeatFor 3 (ParallelLast) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  X  :  Type
2.  Y  :  Type
3.  d  :  metric(X)
4.  d'  :  metric(Y)
5.  A  :  Type
6.  A  \msubseteq{}r  X
7.  x  :  X  {}\mrightarrow{}  Y
8.  x:FUN(X;Y)
\mvdash{}  x:FUN(A;Y)


By

---

Latex:
RepeatFor  3  (ParallelLast)

---

Home Index