---

Step * 1 1 1 1 of Lemma quotient-bind-ext

.....assertion..... 
1. A : Type
2. B : Type
3. a : Base
4. a1 : Base
5. a = a1 ∈ pertype(λx,y. ((x ∈ A) ∧ (y ∈ A) ∧ True))
6. a ∈ A
7. a1 ∈ A
8. True
9. f : Base
10. f1 : Base
11. f = f1 ∈ (A ⟶ ⇃(B))
⊢ (f a) = (f1 a1) ∈ ⇃(⇃(B))
BY
{ ((Assert ⌜f ∈ A ⟶ ⇃(B)⌝⋅ THENA Auto)
   THENM (Assert ⌜f1 ∈ A ⟶ ⇃(B)⌝⋅ THENA Auto)
   THENM (Assert ⌜f a ∈ ⇃(B)⌝⋅ THENA Auto)
   THENM (Assert ⌜f1 a1 ∈ ⇃(B)⌝⋅ THENA Auto)
   THENM Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  Type
3.  a  :  Base
4.  a1  :  Base
5.  a  =  a1
6.  a  \mmember{}  A
7.  a1  \mmember{}  A
8.  True
9.  f  :  Base
10.  f1  :  Base
11.  f  =  f1
\mvdash{}  (f  a)  =  (f1  a1)


By

---

Latex:
((Assert  \mkleeneopen{}f  \mmember{}  A  {}\mrightarrow{}  \00D9(B)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENM  (Assert  \mkleeneopen{}f1  \mmember{}  A  {}\mrightarrow{}  \00D9(B)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENM  (Assert  \mkleeneopen{}f  a  \mmember{}  \00D9(B)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENM  (Assert  \mkleeneopen{}f1  a1  \mmember{}  \00D9(B)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENM  Auto)

---

Home Index