---

Step * of Lemma map-pair-prior

∀[Info,A,B,C,D:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[f:(A × B) ⟶ C]. ∀[g:(A × D) ⟶ C]. ∀[h:B ⟶ D].
  (f[p] where p from X;Y) = (g[p] where p from X;(h[y] where y from Y)) ∈ EClass(C) 
  supposing ∀a:A. ∀b:B.  (f[<a, b>] = g[<a, h[b]>] ∈ C)
BY
{ (Auto
   THEN BLemma `es-interface-extensionality`
   THEN (Auto THEN Try (Complete ((ProveSV THEN Auto)⋅)))
   THEN RWW "map-class-val pair-prior-val" 0
   THEN Auto
   THEN All (\h. RWW "is-map-class is-pair-prior" h )
   THEN Auto
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B,C,D:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[f:(A  \mtimes{}  B)  {}\mrightarrow{}  C].  \mforall{}[g:(A  \mtimes{}  D)  {}\mrightarrow{}  C].
\mforall{}[h:B  {}\mrightarrow{}  D].
    (f[p]  where  p  from  X;Y)  =  (g[p]  where  p  from  X;(h[y]  where  y  from  Y)) 
    supposing  \mforall{}a:A.  \mforall{}b:B.    (f[<a,  b>]  =  g[<a,  h[b]>])


By

---

Latex:
(Auto
  THEN  BLemma  `es-interface-extensionality`
  THEN  (Auto  THEN  Try  (Complete  ((ProveSV  THEN  Auto)\mcdot{})))
  THEN  RWW  "map-class-val  pair-prior-val"  0
  THEN  Auto
  THEN  All  (\mbackslash{}h.  RWW  "is-map-class  is-pair-prior"  h  )
  THEN  Auto
  THEN  Auto)

---

Home Index