--- a/src/ZProduct.agda	Tue Mar 07 09:00:03 2023 +0900
+++ b/src/ZProduct.agda	Tue Mar 07 12:13:21 2023 +0900
@@ -189,6 +189,10 @@
       zz11 : & < * (zπ1 pab) , * (zπ2 pab) > ≡ & < * a , * b >
       zz11 = zp-iso pab
 
+zp-iso0 :  { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (zπ1 p ≡ a) ∧ (zπ2 p ≡ b)
+zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) ))  
+                              , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (zp-iso1 pab) ) )  ⟫
+
 ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
 ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)