---

Step * 1 of Lemma set_prod_wf


1. s : DSet
2. t : DSet
⊢ IsEqFun(|s| × |t|;λa,b. (a =b b))
BY
{ Eval ``eqfun_p`` 0  }

1
1. s : DSet
2. t : DSet
⊢ ∀[x,y:|s| × |t|].  uiff(↑(x =b y);x = y ∈ (|s| × |t|))

---

Latex:

---

Latex:

1.  s  :  DSet
2.  t  :  DSet
\mvdash{}  IsEqFun(|s|  \mtimes{}  |t|;\mlambda{}a,b.  (a  =\msubb{}  b))


By

---

Latex:
Eval  ``eqfun\_p``  0 

---

Home Index