---

Step * 1 of Lemma member-per-product


1. A : Type
2. B : per-function(A;a.Type)
3. a : A
4. b : B[a]
5. per-product(A;a.B[a]) ∈ Type
⊢ <a, b> ∈ per-product(A;a.B[a])
BY
{ (PointwiseFunctionality 3⋅
   THEN PointwiseFunctionality 6⋅
   THEN Repeat (EqCDA)⋅
   THEN (RepUR ``per-product member`` 0
         THEN Refine_pertypeMemberEquality ⌜A⌝⋅
         THEN Try ((RepUR ``per-product`` (-1) THEN Trivial))
         THEN Try (MemBase)
         THEN Reduce 0
         THEN Repeat (DUand 0)
         THEN Try (QuickAuto))
   ⋅) }

1
1. A : Type
2. B : per-function(A;a.Type)
3. a1 : Base
4. b1 : Base
5. c : a1 = b1 ∈ A
6. a : Base
7. b2 : Base
8. c1 : a = b2 ∈ B[a1]
9. per-product(A;a.B[a]) ∈ Type
⊢ Ax ∈ a = b2 ∈ B[b1] supposing b1 = b1 ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  per-function(A;a.Type)
3.  a  :  A
4.  b  :  B[a]
5.  per-product(A;a.B[a])  \mmember{}  Type
\mvdash{}  <a,  b>  \mmember{}  per-product(A;a.B[a])


By

---

Latex:
(PointwiseFunctionality  3\mcdot{}
  THEN  PointwiseFunctionality  6\mcdot{}
  THEN  Repeat  (EqCDA)\mcdot{}
  THEN  (RepUR  ``per-product  member``  0
              THEN  Refine\_pertypeMemberEquality  \mkleeneopen{}A\mkleeneclose{}\mcdot{}
              THEN  Try  ((RepUR  ``per-product``  (-1)  THEN  Trivial))
              THEN  Try  (MemBase)
              THEN  Reduce  0
              THEN  Repeat  (DUand  0)
              THEN  Try  (QuickAuto))
  \mcdot{})

---

Home Index